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

Lasse Jacobsen, Morten Jacobsen & Mikael H. MøLler
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...