Model Checking Safe, Strongly Persistent Petri Nets

System properties can often be expressed as formulae of a temporal logic. In this chapter, a small logic called S4 is introduced, which is however strong enough to express properties such as reachability and liveness. A model checker is an algorithm with two input parameters, deciding the truth or falsehood of a given temporal logic formula with respect to a given system. We shall describe a simple model checking algorithm which allows S4 formulae to be checked on a restricted class of Petri net systems. Eventually, this leads to a polynomial-time algorithm which can check whether a given marked graph satisfies any of the properties expressible in S4.