2026-07-24T18:53:27Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2346 2024-03-06T10:28:42Z ddc:004 open_access

Undecidability of Coverability and Boundedness for Timed-Arc Petri Nets with Invariants Jacobsen, Lasse Jacobsen, Morten Møller, Mikael H. Timed-Arc Petri Nets Undecidability Coverability Boundedness Timed-Arc Petri Nets (TAPN) is a well studied extension of the classical Petri net model where tokens are decorated with real numbers that represent their age. Unlike reachability, which is known to be undecidable for TAPN, boundedness and coverability remain decidable. The model is supported by a recent tool called TAPAAL which, among others, further extends TAPN with invariants on places in order to model urgency. The decidability of boundedness and coverability for this extended model has not yet been considered. We present a reduction from two-counter Minsky machines to TAPN with invariants to show that both the boundedness and coverability problems are undecidable. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lasse Jacobsen and Morten Jacobsen and Mikael H. Møller 2009 Is Part Of OASIcs, Volume 13, Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) (2009) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DROPS.MEMICS.2009.2346 urn:nbn:de:0030-drops-23461 https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2346 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode