On the Existence of Network Invariants for Verifying Parameterized Systems? - Correct System Design: Recent Insights and Advances - page 180

If we further assume that each action of the parameterized system involves a
bounded number of components (i.e., the synchronization predicate does not
contain any occurrence of the superscript

), then the set of predecessors of an
existential assertion can again be expressed as an existential assertion.

!

Having a procedure for calculating pre ( ), a formula that represents the set of

predecessors of states that satisfy , we can now perform symbolic verication

as follows. Assume that final is the existential constraint that represent the set

of undesirable states, and let initial be a characterization of the initial states of

a parameterized system. Typically will contain a universal quantication

over the set of all processes in the network, e.g., saying that they are in their
initial states.

initial

A simple description of an algorithm for checking whether final is reachable

is as follows [KMM + 97]. from initial

Let 0 := final

i ; ; ;:::

For =0 1 2 repeat

i ^ initial

If ( ) = false then return reachable

i +1 := i _ ; i )

Let pre (

until i +1 = i

return unreachable

Note that, under the assumption that each action of the parameterized system
involves a bounded number of components, each i generated by the algorithm

can be expressed as an existential assertion. This follows by induction from
the observation that i +1 is a disjunction of the existential assertions i +1 and

pre ( ; i ).

3.2 Network Invariants

A method, which has been proposed for the verication of innite-state systems,
is to nd a nite-state abstraction of the system, which preserves the correctness
properties of interest, and thereafter model-checking this nite-state abstraction
[LS97,LHR97,ID99]. Adapted to our framework, this would entail the construc-
tion of an abstract process N , whose behavior \contains" the behavior of any

instance M n of the family.

Considering that we are interested in verifying invariants which are universal
assertions, we dene an abstract process to be a process in which each state n is

labeled by an assertion L ( n ) over the states of M . We dene a renement relation

v between networks and abstract processes as follows. We say that M n v N; if

there is a simulation relation R between the states of M n and the states of N

such that

1. Each initial state of M n is related to some state of N ,