On Model Checking Safety Properties

Reference:

Timo Latvala. On model checking safety properties. Research Report A76, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 2002.

Abstract:

Safety properties are an interesting subset of general temporal properties for systems. In the linear time paradigm, model checking of safety properties is simpler than the general case, because safety properties can be captured by finite automata. This work discusses the theoretical and some of the practical issues related to model checking LTL properties.

Our first contribution is a theorem relating abstraction for Coloured Petri nets as defined by Lakos and preservation of safety properties. We show that a subset of the safety properties are preserved for this abstraction framework. Our other contribution is an efficient algorithm for translating LTL safety properties to finite automata. Minor contributions include new proofs for some old complexity results regarding LTL and safety properties.

The implementation of the translation algorithm is also experimentally evaluated. Experiments support the feasibility of the approach. In many tests the implementation is quite competitive when compared to algorithms translating full LTL to Büchi automata. The implementation can also check if an LTL formula is pathologic. The check performs well according to experiments.

Keywords:

Computer aided verification, model checking, LTL, safety properties, abstraction, Coloured Petri nets

Suggested BibTeX entry:

@techreport{HUT-TCS-A76,
    address = {Espoo, Finland},
    author = {Timo Latvala},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {December},
    number = {A76},
    pages = {61},
    title = {On Model Checking Safety Properties},
    type = {Research Report},
    year = {2002},
}

NOTE: Reprint of Licentiate's thesis; see URL below.
PostScript (830 kB)
GZipped PostScript (349 kB)
PDF (471 kB)
See www.tcs.hut.fi ...