Research Report A67: Model Checking Linear Temporal Logic Properties of Petri Nets with Fairness Constraints

Author: Timo Latvala

Date: Jan 2001

Pages: 44

Verification of liveness properties of systems requires in many cases fairness constraints to be imposed on the system. In the context of modeling and analysis with Petri nets, fairness constraints have been defined but the results have not been extended to model checking.

In this work Coloured Petri nets are extended with fairness constraints on the transitions. The semantics of the fairness constraints are defined with a fair Kripke structure. Model checking linear temporal logic (LTL) properties of the Petri net is facilitated by introducing a new LTL model checking procedure. The procedure employs Streett automata to cope with the fairness constraints efficiently. Also, new algorithms for the emptiness checking problem of Streett automata and counterexample generation are presented.

The new procedure has been implemented in the M{\footnotesize ARIA} analyzer. Some experiments are performed to test the implementation and compare it with other ways of coping with fairness constraints. The results show that the procedure scales well when compared to alternative approaches.

Keywords: Computer aided verification, Petri nets, model checking, fairness, Streett automata, counterexamples.

Full report in Postscript
Full report in Portable Document Format