In: Baeten, J.C.M.; et al.: Lecture Notes in Computer Science, Vol. 458; CONCUR'90, Theories of Concurrency: Unification and Extension. (Conference, 1990, Amsterdam, The Netherlands), pages 115-125. Berlin, Germany: Springer-Verlag, 1990.
Abstract: Many interesting concurrent systems, including Petri nets, have infinite state spaces. The question the authors address is: can model checking techniques be extended from finite to infinite state spaces? They provide an affirmative answer by presenting a sound and complete tableau system for proving temporal properties of states (processes or markings) in arbitrary infinite transition system models. The delicate aspect is showing that a point (or set of points) has, or lacks, a least fixed point property (a liveness property).
Keywords: temporal properties (of processes); infinite state space; infinite transition system; fixed point property.