Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Dense-Timed Petri Nets: Checking Zenoness, Token liveness and Boundedness
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
2007 (engelsk)Inngår i: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 3, nr 1, s. 1-61Artikkel i tidsskrift (Fagfellevurdert) Published
Abstract [en]

We consider Dense-Timed Petri Nets (TPN), an extension of Petri nets in which each token is equipped with a real-valued clock and where the semantics is lazy (i.e., enabled transitions need not fire; time can pass and disable transitions). We consider the following verification problems for TPNs. (i) Zenoness: whether there exists a zeno-computation from a given marking, i.e., an infinite computation which takes only a finite amount of time. We show decidability of zenoness for TPNs, thus solving an open problem from [Escrig et al.]. Furthermore, the related question if there exist arbitrarily fast computations from a given marking is also decidable. On the other hand, universal zenoness, i.e., the question if all infinite computations from a given marking are zeno, is undecidable. (ii) Token liveness: whether a token is alive in a marking, i.e., whether there is a computation from the marking which eventually consumes the token. We show decidability of the problem by reducing it to the coverability problem, which is decidable for TPNs. (iii) Boundedness: whether the size of the reachable markings is bounded. We consider two versions of the problem; namely semantic boundedness where only live tokens are taken into consideration in the markings, and syntactic boundedness where also dead tokens are considered. We show undecidability of semantic boundedness, while we prove that syntactic boundedness is decidable through an extension of the Karp-Miller algorithm.

sted, utgiver, år, opplag, sider
2007. Vol. 3, nr 1, s. 1-61
Emneord [en]
Real-time systems, Timed Petri nets, Verification, Zenoness
HSV kategori
Identifikatorer
URN: urn:nbn:se:uu:diva-21144DOI: 10.2168/LMCS-3(1:1)2007ISI: 000262497000001OAI: oai:DiVA.org:uu-21144DiVA, id: diva2:48917
Tilgjengelig fra: 2007-05-21 Laget: 2007-05-21 Sist oppdatert: 2017-12-08bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekst

Søk i DiVA

Av forfatter/redaktør
Abdulla, Parosh Aziz
Av organisasjonen
I samme tidsskrift
Logical Methods in Computer Science

Søk utenfor DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric

doi
urn-nbn
Totalt: 678 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf