On model checking for Petri nets and a linear-time temporal logic
Tomoki Yoneda · 1992
This paper presents an efficient model checking algorithm for Petri nets. It is based on the reduced state space generation where the result of the evaluation on the full state space and the reduced state space is identical. This reduction of the state spaces is possible, because (1) the firings of the transitions are only partially ordered by causality and a given formula, and (2) the order of firings of transitions not related by this partial order is irrelevant for the evaluation of the given formula.