91: Hildesheimer Informatik-Berichte 11, pages 1-22 pp.. Universität Hildesheim (Germany), Institut für Informatik, October 1991.
Abstract: Model checking --- the algorithmic determination of truth or falsehood of a modal or temporal logic formula, given a model --- faces the state explosion problem. The authors investigate the possibility of obtaining model checkers which do not require at all to construct the associated transition sytem, ie model checkers which work directly on the syntax. The authors consider the modal logic S4 and concentrate on safe persistent Petri nets. They show that the model checking problem for this class of nets is polynomially reducible to a simpler problem and prove that for the subclass of safe T-systems this simpler problem can be solved in polynomial time in the size of the system.
Keywords: model checking (of) safe persistent net; temporal logic; state explosion problem; modal logic; polynomial time solution.