Reference:

E. Best and J. Esparza. Model checking of persistent Petri nets. In G. Jäger E. Börger, H. Kleine Büning, and M. M. Richter, editors, Proceedings of Computer Science Logic, number 626 in Lecture Notes in Computer Science, pages 35–52, 1991.

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.

Suggested BibTeX entry:

@inproceedings{BE91,
    author = {E. Best and J. Esparza},
    booktitle = {Proceedings of Computer Science Logic},
    editor = {E. ~B{\"o}rger, G. ~J{\"a}ger and H. ~Kleine B{\"u}ning and M. M. ~Richter},
    number = {626},
    pages = {35-52},
    series = {{Lecture Notes in Computer Science}},
    title = {Model Checking of Persistent {P}etri Nets},
    year = {1991}
}