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

Currently, much eort is devoted to advancing further the power of automated
verication to cover also innite-state systems. Potentially practical tools for
automated verication of innite-state systems have been developed for signi-
cant special cases, such as timed automata [ACD90,BGK + 96], hybrid automata
[Hen95], data-independent systems [JP93,Wol86], Petri nets [JM95], pushdown
processes [BS95,Sti96], and systems with unbounded communication channels
[Fin94,AJ93,ABJ98].

On the border between nite-state and innite-state systems, there is the class of
parameterized systems . By a parameterized system, we mean a family of similar
systems that depend in a regular way on a parameter. Typically, parameter-
ized systems are built from a (small) nite set of processes, which are replicated
and interconnected into networks. Examples of parameterized systems abound:
a distributed algorithm can be modeled as a system of many identical processes
whose interconnection topology may be arbitrary, a bus protocol consists of a
linear array of identical processes where the parameter is the number of pro-
cesses, etc. Also unbounded data structures, such as queues and trees, could be
regarded as parameterized systems by letting each node (cell) be viewed as a
process which is connected to its neighbour nodes (cells). A queue would thus
be viewed as a linear array of processes of arbitrary length.

In order to make the discussion more concrete, let us consider families of systems
of the form

P 0 k P k P k k P

composed of one instance of a \global" component P 0 which is common to all sys-

tems in the family, and an arbitrary number of instances of some process P .The

k

processes are composed by some associative composition operator , which for

the moment will be left unspecied. The verication problem for parameterized
systems consists in verifying that

P 0 k P k P k k P j =

P

for some correctness formula , for any number of copies of . We assume

that the formulation of is independent of the system size. An example of a

correctness property could be \there are never two processes simultaneously in
the critical section".

The most straight-forward approach to verifying a parameterized system is to
verify the system for a suitable chosen number (say 5) of processes. Finite-state
state-space exploration methods can be used to analyze the system eciently.
However, there is no a priori guarantee that the system will function correctly
with 6 processes. It is therefore of interest to consider methods that verify the
correctness of the system with an arbitrary number of components. It may even
(as argued, e.g., by Wolper and Boigelot [WB98]) turn out that the parameter-
ized version of the system is easier to verify, since in the best case it may concern
the essential reason for correctness, and avoid the particularities of the case with
5 processes.