Information Technology Reference
In-Depth Information
a
−! s
0
is a
2. whenever
sRn
for a state
s
of
M
n
and a state
n
of
N
, and if
s
a
−! n
0
of
s
0
Rn
0
,
transition of
M
n
, then there is a transition
n
N
with
3. whenever
sRn
,then
s
satises the assertion
L
(
n
).
N v N
0
if
We also dene
v
to a preorder on abstract processes, by saying that
N
0
in the usual sense such that
there is a simulation
R
between states of
N
and
nRn
0
for a state
n
0
of
N
0
, then the assertion
whenever
n
of
N
and a state
n
0
).
L
(
n
) implies the assertion
L
(
A methodology, which has been proposed [KM89,WL89], is to nd a process
N
,
for which the above relation can be checked by induction, checking
1.
P
0
v N
,
2.
N k P v N
,and
3.
is implied by each assertion that labels some control state of
N
The composition
N k P
between an abstract process
N
and a component process
P
is dened in the standard way. Each state of
N k P
is obtained as a composition
n k t
, which is labeled by an assertion which
states that \all processes except the last one satisfy
of a state
n
of
N
and a state
t
of
P
L
(
n
), and the last process
is in state
t
". For instance, if
L
(
n
) is \at most one process has the token" and
t
is a state where process
P
has the token, then
L
(
n k t
) could be \one or two
processes have the token, and one of these is in state
t
".
It should be noted that each
here are considered as open systems, in
the sense of Section 2. Thus in the rst condition
M
n
and
N
P
0
v N
, the component
P
0
is
regarded as an open system so that
must be able to simulate all its potential
synchronizations with other components.
N
We dene a
network
invariant to be an abstract process which satises the two
rst conditions. A network invariant is said to be
suciently strong
if it also sat-
ises the third condition. There is a least network invariant
N
: this is the \union"
of all
which satises the two last conditions: this is
the limit of the so-called quotient construction [And95,KLL
+
97]. However, there
is no guarantee that any of these be expressible by a nite-state program even
if
M
n
. There is also a largest
N
P
0
and
P
N
is therefore often per-
formed manually (as e.g., in [WL89,KM89]), or using approximation techniques
[LHR97].
are nite-state. The discovery of a suitable
Example
A suciently strong network invariant of the system in the preceding
section is the nite-state process
rec-token
send-token
Search WWH ::
Custom Search