{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:06Z","timestamp":1753889766535,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2007,2,7]],"date-time":"2007-02-07T00:00:00Z","timestamp":1170806400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We consider Dense-Timed Petri Nets (TPN), an extension of Petri nets in which\neach token is equipped with a real-valued clock and where the semantics is lazy\n(i.e., enabled transitions need not fire; time can pass and disable\ntransitions). We consider the following verification problems for TPNs. (i)\nZenoness: whether there exists a zeno-computation from a given marking, i.e.,\nan infinite computation which takes only a finite amount of time. We show\ndecidability of zenoness for TPNs, thus solving an open problem from [Escrig et\nal.]. Furthermore, the related question if there exist arbitrarily fast\ncomputations from a given marking is also decidable. On the other hand,\nuniversal zenoness, i.e., the question if all infinite computations from a\ngiven marking are zeno, is undecidable. (ii) Token liveness: whether a token is\nalive in a marking, i.e., whether there is a computation from the marking which\neventually consumes the token. We show decidability of the problem by reducing\nit to the coverability problem, which is decidable for TPNs. (iii) Boundedness:\nwhether the size of the reachable markings is bounded. We consider two versions\nof the problem; namely semantic boundedness where only live tokens are taken\ninto consideration in the markings, and syntactic boundedness where also dead\ntokens are considered. We show undecidability of semantic boundedness, while we\nprove that syntactic boundedness is decidable through an extension of the\nKarp-Miller algorithm.<\/jats:p>","DOI":"10.2168\/lmcs-3(1:1)2007","type":"journal-article","created":{"date-parts":[[2008,6,3]],"date-time":"2008-06-03T11:43:37Z","timestamp":1212493417000},"source":"Crossref","is-referenced-by-count":11,"title":["Dense-Timed Petri Nets: Checking Zenoness, Token liveness and Boundedness"],"prefix":"10.46298","volume":"Volume 3, Issue 1","author":[{"given":"Parosh","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Pritha","family":"Mahata","sequence":"additional","affiliation":[]},{"given":"Richard","family":"Mayr","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2007,2,7]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/2223\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/2223\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:09:54Z","timestamp":1681243794000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/2223"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2,7]]},"references-count":0,"URL":"https:\/\/doi.org\/10.2168\/lmcs-3(1:1)2007","relation":{"is-same-as":[{"id-type":"arxiv","id":"cs\/0611048","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.cs\/0611048","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2007,2,7]]},"article-number":"2223"}}