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

putational and network invariants. In the case of computational invariants, we
will take this to mean an invariant which considers an arbitrary \nite" part
of the system structure. In the case of network invariants, we will take this to
mean an invariant which can be expressed by a nite-state transition system.
As observed by Wolper and Lovinfosse [WL89], it follows from a basic unde-
cidability result by Apt and Kozen [AK86], that such invariants do not exist in
general. In this paper, we will give some sucient criteria for the existence of
these invariants. We hope that this gives a better understanding in particular of
the network invariant method. Mechanized search for network invariants have
been considered by Lesens et al [LHR97], who employ maximal xpoint iteration,
enhanced by approximation techniques, in the verication of some examples. Ab-
stractions can also be constructed without checking that it is in inductive, e.g.,
as in [LS97,CGJ95]. German and Sistla [GS92] have given a direct algorithm for
model-checking of parameterized systems with an unordered system topology, in
a slightly more restricted framework than that considered here.

The paper is organized as follows. In the next section, we introduce the ba-
sic denitions of parameterized systems. The use of invariants in verication is
described in Section 3. Section 4 contains criteria for the existence of compu-
tational and network invariants. In Section 5, we illustrate the verication of
a parameterized system in which the components are non-nite state (timed
automata).

2 Basic Denitions

Parameterized Systems By a parameterized system, we mean a family of systems,
each of which is a composition of form

M n P 0 k P k P k k P n

[1] [2] [ ]

P 0 is an optional \global" component, common to all instances in the
family, and where

where

P ;:::;P n P i

[1] [ ] are identical processes. Each component [ ]

P 0 is modeled as a labeled transition system. For the moment, we do not
require that each component be nite-state. The labels on transitions are taken
from a set of visible actions, extended by an invisible action (denoted

and

). We
assume that any component can always perform an idling component transition,
labeled by , which does not change its state. We use M to denote the (innite-

fM n g n =0 of system instances.

state) system which is the \union" of the family

One could think of M as a system, which initially decides on a value of the

parameter n , and then becomes M n .

Each transition of the system M n may involve one or more components. The pos-

sible synchronizations between components are constrained by a synchronization
predicate . In the remainder of this paper, we will consider a totally unordered

system topology, in which any component can communicate with any other,