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.
