Model checking of persistent petri nets

Abstract

In this paper we develop a model checking algorithm which is fast in the size of the system. The class of system models we consider are safe persistent Petri nets; the logic is S4, i.e. propositional logic with a ‘some time’ operator. Our algorithm does not require to construct any transition system: We reduce the model checking problem to the problem of computing certain Parikh vectors, and we show that for the class of safe marked graphs these vectors can be computed- from the structure of the Petri net - in polynomial time in the size of the system.