Information Technology Reference
In-Depth Information
where the two left states are labeled by the assertion
8i: :
c
[
i
] and where the
right state is labeled by the assertion
8i 6
=
j: :
(
c
[
i
]
^
c
[
j
]). We note that
the disjunction of all
L
(
n
) for states
n
of the network invariant need not be a
computational invariant of
. It can be weaker, as long as we can check the
invariant to be veried on the basis of these labels.
M
4
Generating Simple Invariants
In this section, we shall consider the question of nding a computational or
network invariant of a particularly simple form. Recall that we only consider the
verication of invariants expressed by universal assertions.
4.1
Universal Computational Invariants
We shall be concerned with nding computational invariants that are universal.
For instance, in the small mutual exclusion example, it was possible to nd a
universal invariant. From results by Abdulla et al. [ACJYK96], the following
theorem follows directly.
P
0
and
P
Theorem 1.
If
are nite-state, and all synchronizations occur be-
tween a bounded number of components, then the largest invariant is universal.
Furthermore, it (or rather its negation) can be found after a nite number of
iterations of the backward reachability algorithm in Section 3.1.
The main reason why the backward reachability algorithm terminates is that it is
impossible to generate a strictly increasing and innite sequence
0
;
1
;
2
;
3
;:::
of existential assertions. Any such sequence will converge to a largest set after a
nite number of iterations. This can be seen as follows. Since we are considering
an unordered system topology, a system state can be represented as a multiset
of states of
. Each existential assertion denotes an
upward closed
(wrp.
to multiset inclusion) set of system states. By Dickson's lemma [Dic13], any
upward closed set of multisets can be represented by a
nite
set of minimal
elements (multisets). When we apply this to an innite sequence
P
0
and
P
0
;
1
;
2
;
3
;:::
of upward closed sets of multisets, it follows that its limit is also upward closed,
and that the nitely many minimal elements that characterize this limit must
be included after a nite number of iterations.
These results have been extended to cover a class of nite-state systems that
allow also broadcast [EFM99], and to timed automata with one clock in [AJ98].
For a slightly more restrictive framework, German and Sistla [GS92] have given
an algorithm for model-checking arbitrary temporal properties of the controller.
Search WWH ::
Custom Search