Undecidability of LTL for Timed Petri Nets

Parosh Aziz Abdulla and Aletta Nylen


Abstract

We show undecidability of (action based) linear temporal logic (LTL) for timed Petri nets. This is to be contrasted with decidability of both the problem of checking safety properties for timed Petri nets, and the problem of checking LTL formulas for (untimed) Petri nets. The undecidability result is shown through a reduction from a similar problem for lossy counter machines [Mayr00].