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.