For the most recent entries see the Petri Nets Newsletter.

Proving Temporal Properties of Petri Nets.

Bradfield, J.C.

In: Proceedings of the 11th International Conference on Application and Theory of Petri Nets, 1990, Paris, France, pages 315-331. 1990.

Also in: Rozenberg, G.: Lecture Notes in Computer Science, Vol. 524; Advances in Petri Nets 1991, pages 29-47. Berlin, Germany: Springer-Verlag, 1991.

Abstract: The author presents a sound and complete tableau system for proving temporal properties of Petri nets, expressed on a propositional mu-calculus which subsumes many other temporal logics. The system separates the checking of fix-points from the rest of the logic, which allows the use of net-specific analysis for this, especially to prove liveness and fairness properties. The proofs of soundness and completeness are given in detail.

Keywords: temporal properties (of nets); propositional mu-calculus; logic fix-point; temporal logic; liveness; fairness; soundness; completeness; tableau system; model-checking.

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

Back to the Petri Nets Bibliography