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

occurrences of each control state of ]. In the case of a linear network, regular

expressions could serve this purpose [CGJ95,KMM + 97,ABJN99].

P [ i

The requirements on a computational invariant I are:

1. any initial state of any ,

2. each transition from a system state satisfying

M n satises I

I leads to a system state which

also satises I .

We say that I is suciently strong if additionally

3. I implies .

It is a standard result that the set of invariants that satisfy these requirements

form a lattice. The lattice is non-empty if and only if

I

is an invariant of M n for

all (with respect to set-inclusion)

which satises the rst two conditions: this is the set of reachable states of

n . There is a least computational invariant I

M

.

I

There is also a largest which satises conditions 2. and 3.

It is well-known that a suciently strong computational invariant always exists
if M n , but there is no guarantee that it can in gen-

eral be expressed in the particular chosen representation (this follows from the
undecidability of parameterized system verication [AK86]). Methods for auto-
matically searching for computational invariants include forward and backward
reachability analysis, sometimes augmented by approximation techniques, using
a symbolic representation of sets of states.

is an invariant of each

In what follows, we shall be particularly interested in nding computational
invariants that are expressed as universal assertions . It turns out that backward
reachability analysis suits the problem of nding universal assertions.

Example To continue the example in the previous section, we see that a su-
ciently strong computational invariant of any M n is

8i 6 = j: : [( t [ i ] _ c [ i ]) ^ ( t [ j ] _ c [ j ])]

which is indeed a universal assertion.

Below, we describe the relation to backward reachability in more detail.

Backward Reachability Analysis The basic idea of backward reachability analysis
is to start from the negation of the invariant to be checked. If the invariant is a
universal assertion, then the negation is an existential assertion. We assume that
we can represent sets of states of an arbitrary but bounded set of components.
The idea in backward reachability analysis is to compute the set of states from
which a state satisfying the negated invariant can be reached.