Sökning: onr:"swepub:oai:DiVA.org:uu-529342" >
Decidability of Zen...
Decidability of Zenoness, Token Liveness and Boundedness of Dense-Timed Petri Nets
-
- Abdulla, Parosh (författare)
- Uppsala universitet,Institutionen för informationsteknologi
-
Mahata, Pritha (författare)
-
Mayr, Richard (författare)
-
(creator_code:org_t)
- Department of Information Technology, Uppsala University, 2004
- Engelska.
-
Serie: Technical report / Department of Information Technology, Uppsala University, 1404-3203 ; 2004-034
- Relaterad länk:
-
https://uu.diva-port... (primary) (Raw object)
-
visa fler...
-
https://urn.kb.se/re...
-
visa färre...
Abstract
Ämnesord
Stäng
- We consider 'Timed Petri Nets (TPNs)' : extensions of Petri nets in which each token is equipped with a real-valued clock. We consider the following three verification problems for TPN. (i) 'Zenoness:' whether there is an infinite computation from a given marking which takes only a finite amount of time. We show decidability of zenoness for TPNs, thus solving an open problem from \citeEscrig:etal:TPN. (ii) 'Token liveness:' whether a token is ıt 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Publikations- och innehållstyp
- vet (ämneskategori)
- rap (ämneskategori)