Application of weaker simulations to parameterized model checking by network invariants

I. V. Konnov

Modelirovanie i analiz informacionnyh sistem, Tome 15 (2008) no. 3, pp. 3-13

Résumé

In this paper, we consider parameterized model checking problem of asynchronously communicating processes in the framework of network invariants. The framework of network invariants exploits relations over labelled transition systems such as simulation, bisimulation, trace equivalence and trace inclusion. In the case of asynchronous parallel composition simulation and bisimulation are supposed to be rather strong and additional abstractions are required. In our work three weaker simulation relations are proposed: quasi-block simulation, block simulation and semi-block simulation. Quasi-block simulation has all the properties to be applied in the framework of network invariants. Block simulation is a stronger relation than a quasi-block simulation. It is used to find an invariant. An initial block simulation over two models exists if and only if an initial semi-block simulation over that models exists. Thus, it is sufficient to compute a semi-block simulation on the models. The sketch of an algorithm to perform such a computation is presented. Previously, we used the framework to check a parameterized model of RSVP protocol. In this paper a series of optimizations that decrease the time of computation are shown.