1 Search Results for "Jacobsen, Morten"

Document
DOI: 10.4230/DROPS.MEMICS.2009.2346
Undecidability of Coverability and Boundedness for Timed-Arc Petri Nets with Invariants

Authors: Lasse Jacobsen, Morten Jacobsen, and Mikael H. Møller

Published in: OASIcs, Volume 13, Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) (2009)

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.
Cite as

Lasse Jacobsen, Morten Jacobsen, and Mikael H. Møller. Undecidability of Coverability and Boundedness for Timed-Arc Petri Nets with Invariants. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 106-113, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{jacobsen_et_al:OASIcs:2009:DROPS.MEMICS.2009.2346,
  author =	{Jacobsen, Lasse and Jacobsen, Morten and M{\o}ller, Mikael H.},
  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 =	{106--113},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.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}
}
  • Refine by Author
  • 1 Jacobsen, Lasse
  • 1 Jacobsen, Morten
  • 1 Møller, Mikael H.

  • Refine by Classification

  • Refine by Keyword
  • 1 Boundedness
  • 1 Coverability
  • 1 Timed-Arc Petri Nets
  • 1 Undecidability

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2009

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact