For the most recent entries see the Petri Nets Newsletter.

Verifying Temporal Properties of Processes.

Bradfield, J.; Stirling, C.

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.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography