On the decidability of model checking LTL fragments in monotonic extensions of Petri nets

Abstract

We study the model checking problem for monotonic extensions of Petri Nets, namely for two extensions of Petri nets: reset nets (nets in which places can be emptied by the firing of a transition with a reset arc) and ν-Petri nets (nets in which tokens are pure names that can be matched with equality and dynamically created). We consider several fragments of LTL for which the model checking problem is decidable for P/T nets. We first show that for those logics, model checking of reset nets is undecidable. We transfer those results to the case of ν-Petri nets. In order to cope with these negative results, we define a weaker fragment of LTL, in which negation is not allowed. We prove that for that fragment, the model checking of both reset nets and ν-Petri nets is decidable, though with a non primitive recursive complexity. Finally, we prove that the model checking problem for a version of that fragment with universal interpretation is undecidable even for P/T nets.