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

If we look at the problem of actually verifying correctness for any number of
copies of , we notice that the problem has an unbounded structure along two

dimensions. One dimension is \time", since we must check a property of po-
tentially unbounded execution sequences. Another dimension is \space", since
the property should hold for an arbitrary system size. To verify that the system
is correct, in spite of any of these unboundednesses, we may use induction. In
the following two paragraphs, we describe the use of induction, rst in the time
dimension and then in the space dimension. Throughout the paper, we will only
be concerned with safety properties.

P

The standard way to handle the time dimension in verication of safety proper-
ties (e.g., [MP95]) is to nd an (inductive) invariant of the system, which is pre-
served by all computation steps of the system, and which implies . For instance,

if is the correctness property \there are never two processes simultaneously in

the critical section", then an inductive invariant of the system could be obtained
by conjoining \at most one process has the token" (assuming that possessing the
token is necessary for entering the critical section). This method of verication
assumes that we can express sets of system states of arbitrary size. Finding an in-
variant may involve some ingenuity. However, once it is found, the rest of the ver-
ication is relatively simple and possible to automate. Computational invariants
expressed in some formalism for represented sets of states of unbounded system
sizes have been used e.g., in [JK95,KMM + 97,EFM99,ACJYK96,AJ98,ABJN99].

A method for handling the space dimension in parameterized system verication
is to nd a uniform abstraction of the system which is independent of system size.
Such an abstraction is a single system whose behavior \contains" (in a sense to

be made more precise later in the paper) the behavior of any system in the family.
In particular, if

N

N j = ,then P 0 kPk k P j = for any system size. One

sucient criterion for checking that N is indeed an abstraction is to check that

it is inductive. Letting denote the relation \contained in", this means that it

P 0 N N k P N N j

should be checked that and that besides checking that =

. The term \network invariant" has been introduced by Wolper and Lovinfosse
[WL89] (the method was also suggested by Kurshan and McMillan [KM89]) for
an abstraction which is inductive in this sense. Again, nding a network invariant
N is found, the

correctness checks should be relatively simple and possible to automate. Network
invariants have been employed in e.g., [KM89,WL89,EN95,LHR97].

may involve some ingenuity. However, the point is that once N

For verifying a parameterized system, there are thus two basically dierent ways
to employ induction: either using standard (computational) induction, or using
induction over the structure of the parameterized system. To avoid confusion,
we will use the term computational invariant to mean an inductive invariant in
the \time-dimension".

In this paper, we will consider the question \when does there exist a computa-
tional or network invariant of a certain simple form?" If we consider the case
that each component is nite-state, it is natural to try to look for \nite" com-