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

Timed-Arc Petri Nets (TAPN) is a well studied extensionof the classical Petri net model where tokens are decorated with realnumbers that represent their age. Unlike reachability, which is known tobe 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 orderto model urgency. The decidability of boundedness and coverability forthis extended model has not yet been considered. We present a reduc-tion from two-counter Minsky machines to TAPN with invariants to showthat both the boundedness and coverability problems are undecidable.