On Application of Weaker Simulations to Parameterized Model Checking by Network Invariants Technique

摘要

In this paper we consider parameterized model checking problem of asynchronous communicating processes in the framework of network invariants. The framework of network invariants relies on relations over labelled transition systems such as simulation, bisimulation, trace equivalence and trace inclusion. In the case of asynchronous parallel composition simulation and bisimulation appear to be rather strong and thus require additional abstractions. In our work three weaker simulation relations are proposed namely quasi-block simulation, block simulation and semi-block simulation. Quasi-block simulation has all the properties to be applied to the technique of network invariants. Block simulation is a stronger relation than a quasi-block simulation. It is used to find an invariant. An initial semi-block simulation over two models exists if and only if an initial 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.