A Unified Model Checking Approach for Safety Properties of Parameterized Systems

Monika Maidl

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


We present a model checking algorithm for safety properties that is applicable to parameterized systems and hence provides a uniform approach of model checking for parameterized systems. By analyzing the conditions under which the proposed algorithm terminates, we obtain a characterization of a class for which this problem is decidable. Token rings and broadcast systems, for which decidability of model checking of safety properties has been shown, fall in our class. The main novel feature in our class is that (unnested) quantification over index variables is allowed. This means that global guards can be expressed. The usefulness of this generalization is illustrated by applying the algorithm to the Bakery algorithm and broadcast protocols with global conditions.

Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems