Model Checking Safety Properties

摘要

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 Colored 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 Buchi automata. The implementation can also check if an LTL formula is pathologic. The check performs well according to experiments.