Two Techniques of Parameterized Model Checking and Symmetry Reduction

Date: Thursday, April 21, 2011
Speaker: Igor V. Konnov
Venue: TU Vienna

Despite acknowledged success of model checking, its application faces several problems generally inherent to the approach. In this talk we address such problems as parameterized model checking and combinatorial state explosion.

The uniform verification problem is to prove that a temporal property is satisfied on every instance of a system composed of an arbitrary number of homogeneous processes. We extend the network invariants technique by introducing three simulation relations on labelled transition systems (LTSs) that capture correspondence between paths of two systems with different number of processes. This allows us to apply the technique to parameterized families of LTSs generated by a network grammar in the asynchronous setting.

Using this extension we implemented CheAPS, the checker of asynchronous parameterized systems. The tool iteratively generates candidate invariants of a parameterized family and then it checks invariance property by constructing a semi-block simulation on a few finite LTSs. As soon as required invariant LTSs are found, these are passed to Spin for finite-state model checking.

Our tool, like many others, suffers from the state explosion effect. This observation and a case study of Generic Attribute Registration Protocol brought us to the investigation of symmetry reduction techniques. One recent method in this field, which allows one to check safety properties is lazy symmetry reduction. It copes with partially symmetric systems by refining abstract state space on-the-fly, where abstraction is built w.r.t. symmetry preserving constraints.

We found that the spirit of the original search algorithm is close to the well-known nested depth first search. This enables integration of lazy symmetry reduction into the algorithm of checking a linear temporal logic formula against a finite-state LTS. However, a great care should be taken when performing lasso detection on the abstract state space. To this end we introduced special notions of pseudo-cycles and feasibility conditions that provided us with the basis for proving soundness and completeness of the new algorithm.

The next bold step is the implementation of the algorithm in Spin. As it is heavily optimized for a specific set of techniques, embedding a new one in this tool is a technical challenge. We believe that in general implementation is close to completion, though its experimental evaluation is still in progress.

Posted in RiSE Seminar