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

Morten Jacobsen, Lasse Jacobsen, Mikael Harkjær Møller

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

206 Downloads (Pure)

Abstrakt

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 decid-
able. 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 reduc-
tion from two-counter Minsky machines to TAPN with invariants to show
that both the boundedness and coverability problems are undecidable.
OriginalsprogEngelsk
TidsskriftOpenAccess Series in Informatics
Vol/bind12
Antal sider8
ISSN2190-6807
DOI
StatusUdgivet - dec. 2009

Fingeraftryk Dyk ned i forskningsemnerne om 'Undecidability of Coverability and Boundedness for Timed-Arc Petri Nets with Invariatnts'. Sammen danner de et unikt fingeraftryk.

Citationsformater