License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/DROPS.MEMICS.2009.2346
URN: urn:nbn:de:0030-drops-23461
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2009/2346/
Go to the corresponding OASIcs Volume Portal

Jacobsen, Lasse ; Jacobsen, Morten ; Møller, Mikael H.

Undecidability of Coverability and Boundedness for Timed-Arc Petri Nets with Invariants

pdf-format:
09006.JacobsenLasse.2346.pdf (0.5 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{jacobsen_et_al:OASIcs:2009:2346,
  author =	{Lasse Jacobsen and Morten Jacobsen and Mikael H. M\oller},
  title =	{{Undecidability of Coverability and Boundedness for Timed-Arc Petri Nets with Invariants}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{104--111},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Petr Hlinen{\'y} and V{\'a}clav Maty{\'a}{\v{s}} and Tom{\'a}{\v{s}} Vojnar},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2009/2346},
  URN =		{urn:nbn:de:0030-drops-23461},
  doi =		{10.4230/DROPS.MEMICS.2009.2346},
  annote =	{Keywords: Timed-Arc Petri Nets, Undecidability, Coverability, Boundedness}
}

Keywords: Timed-Arc Petri Nets, Undecidability, Coverability, Boundedness
Collection: Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)
Issue Date: 2009
Date of publication: 15.12.2009

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI