LTL Model Checking with Logic Based Petri Nets

In this paper we consider unbounded model checking for systems that can be specified in Linear Time Logic. More precisely, we consider the model checking problem “N | = α”, where N is a generalized Petri net (SLPN) (which we have introduced in previous work), and α is an LTL formula. We solve this problem by using results about the equivalence of LTL formulae and Büchi automata