Information Technology Reference
In-Depth Information
Proof. The rst condition
is an abstraction.
To check the second condition, consider the parallel composition
P 0 v N
follows from the fact that
N
N k P
of
N
and
P
. We shall prove that there exists an abstraction mapping
g
from states of
N k P
, from which the theorem follows. We rst observe that an inductive
abstraction mapping
to
N
h
from states of
M
to states of
N
induces a mapping
g
from
N k P
N
g
h
s
k t
h
skt
s
states of
to states of
by letting
(
(
)
)=
(
), where
is a state
M
t
P
s k t
s
M
of
and
is a state of
, and where
denotes the state
of
extended
with one extra component in state
t
. The mapping
g
is well-dened since
h
is
inductive. It can also be checked that
g
is indeed an abstraction mapping.
1. If
n
and
t
are initial, then
n
=
h
(
s
) for some initial
s
,andso
g
(
nkt
)=
h
skt
(
) is initial.
n k t −! n 0
k t 0 is a transition of
s −! s 0
2. If
N k P
, then there is a transition
skt−! s 0
k t 0 is a transition of
of
M
with
h
(
s
)=
n
and
h
(
s 0 )=
n 0 .Thus
s 0
k t 0 )=
n 0
k t 0 ) is a transition
M
, and hence
h
(
s k t
)
−! h
(
g
(
nkt
)
−! g
(
of
N
.
Finally, by the second condition of Denition 1, the the conjunction of the asser-
tion
L
(
h
(
s
)) and the fact that the last process is in state
t
implies the assertion
L
(
h
(
s k t
)).
We will apply this theorem to obtain a result concerning the existence of nite-
state abstraction mappings.
Theorem 3. Assume that
are nite-state, and that there is a su-
ciently strong universal computational invariant which proves that
P 0 and
P
satises
the invariant. Then there is a suently strong nite-state network invariant.
M
Proof. Assume that that the computational invariant has
k
quantied variables.
For each mapping from component states of
P 0 and
P
to the set
f
0
;
1
;:::;k;1g
,
thereisastateof
N
. Label each state of
N
by the conjunction of assertions of
form \there are at most
i
occurrences of component state
t
" for each compo-
nent state
t
which is mapped to some
i
dierent from
1
. Dene an abstraction
mapping
h
from states of
M
to states of
N
, by mapping each state
s
of
M
to
the state of
N
which corresponds to the number of occurrences of component
states of
into an abstract process
by inserting transitions and initial states, as required by the conditions on the
abstraction function
s
,where
1
means \more than
k
". Make
N
is inductive. Moreover, the
computational invariant corresponds to a set of equivalence classes of
h
.Itcannowbecheckedthat
h
N
whose
labeling imply the invariant to be veried. Hence
N
is also suciently strong.
We have thus shown that if there is a universal computational invariant, then
there also exists a nite-state network invariant.
 
Search WWH ::




Custom Search