TCS / Research / Publications / Model Checking Linear Temporal Logic Properties of Petri Nets with Fairness Constraints
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

Model Checking Linear Temporal Logic Properties of Petri Nets with Fairness Constraints

Reference:

Timo Latvala. Model checking linear temporal logic properties of Petri nets with fairness constraints. Research Report A67, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, January 2001.

Abstract:

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 Mfootnotesize 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

Suggested BibTeX entry:

@techreport{HUT-TCS-A67,
    address = {Espoo, Finland},
    author = {Timo Latvala},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {January},
    number = {A67},
    pages = {44},
    title = {Model Checking Linear Temporal Logic Properties of {P}etri Nets with Fairness Constraints},
    type = {Research Report},
    year = {2001},
}

NOTE: Reprint of Master's thesis; see URL below.
PostScript (694 kB)
GZipped PostScript (297 kB)
PDF (548 kB)
See www.tcs.hut.fi ...

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 19 January 2010.