Information Technology Reference
In-Depth Information
4.2
Finite-State Network Invariants
Let us thereafter consider network invariants. A natural desideratum is that
such an invariant should not be more dicult to analyze than a component
process
. That is, if the processes are nite-state, then the network invariant
should be nite-state. In the running example of Section 3, it was easy to nd
a nite-state abstraction. However, Wolper and Lovinfosse [WL89] observe that
by basic undecidability results [AK86], there must be cases where a network
invariant does not exist (at least if we assume that linearly structured networks
are also allowed). In this section, we will present conditions under which their
existence can be guaranteed.
P
To this end, let us employ a standard framework for describing abstractions of
concurrent systems. The abstraction
N
will be generated by collecting states of
M
into equivalence classes. This can be described by an abstraction mapping
h
from states of the family
[Lam89]. Essentially, an abstraction
mapping is a simulation relation which is also a function. The condition for
M
to states of
N
N
to be an abstraction is then that
1.
h
(
s
) is an initial state of
N
whenever
s
is an initial state of
M
,
a
a
−! h
−! s
0
is a transition of
s
0
) is a transition of
s
M
h
s
N
2. if
then
(
)
(
,
3.
s
satises the assertion that labels
h
(
s
).
N
We will now investigate conditions for when the process
is a suciently strong
N
network invariant. Note that not all abstractions
are good enough. For in-
N
stance, the trivial
which has only one state with self-loops for all actions will
in general either not be inductive, or not strong enough. In the running example
of Section 3, the single state of such a process would have to be labeled by an as-
sertion which implies mutual exclusion (in order to be strong enough) but allows
one process to be in its critical section. However, when composed in parallel with
acopyof
P
that moves from state
t
to state
c
, and the resulting composed state would then
not satisfy the assertion of the state of
P
, it would also have to be able to synchronize with a transition of
N
(since it implies mutual exclusion).
Denition 1.
An abstraction mapping is
inductive
if
1. whenever
h
(
s
1
)=
h
(
s
2
)
, then for any state
t
of
P
we have
h
(
s
1
k t
)=
)
,and
2. the conjunction of the assertion
h
(
s
2
kt
L
(
h
(
s
))
and the fact that the last process is
in state
t
implies the assertion
L
(
h
(
s k t
))
.
Inductive abstraction mappings generate inductive abstractions, as shown by the
following:
Theorem 2.
An abstraction
N
of
M
which is obtained from
M
by an inductive
abstraction function, is an inductive network invariant.
Search WWH ::
Custom Search