Information Technology Reference
In-Depth Information
where
B
=
γ
1
[
N
]
∪
γ
2
[
N
]
is the set of blocked actions and
C
=
{
γ
1
(
n
)
|
γ
2
(
n
)
→
n
|
n
∈N}
is the set of communications.
We are now in a position to formulate a soundness result for our translation with
respect to the parallel composition combined with appropriate synchronization,
steps 1 and 2 of our translation. Lemma 1 states that the
mCRL2
process asso-
ciated to a synchronized product of two constraint automata is the same as the
synchronized merge of the
mCRL2
processes corresponding to the two individual
constraint automata. For brevity we restrict to the case of a binary product.
However, the result straightforwardly generalizes to an arbitrary number of con-
stituents. Here, equality is modulo strong bisimulation [11], notation
.Itis
noted that from a logical point of view, branching bisimilar processes, hence
also strongly bisimilar processes, can be used interchangeably within the
mCRL2
toolset.
↔
→
2
,s
0
)
be two con-
straint automata with disjoint sets of port names and let
γ
be a port synchro-
nization for
→
1
,s
0
)
and
Lemma 1.
Let
A
1
=(
S
1
,
N
1
,
A
2
=(
S
2
,
N
2
,
A
1
and
A
2
. Then it holds that
proc
(
A
1
,s
1
)
γ
proc
(
A
2
,s
2
)
↔ proc
(
A
1
γ
A
2
,
s
1
,s
2
)
.
Proof.
We verify, by checking the usual transfer conditions, that the relation
R
=
{
(
proc
(
A
1
,s
1
)
γ
proc
(
A
2
,s
2
)
,
proc
(
A
1
γ
A
2
,
s
1
,s
2
|
s
1
∈A
1
,s
2
∈A
2
}
))
is a strong bisimulation relation. For brevity we write
proc
i
(
s
i
)for
proc
(
A
i
,s
i
),
i
=1
,
2, and
proc
(
s
1
,s
2
)for
proc
(
A
1
γ
A
2
,
s
1
,s
2
).
N
→
Suppose
proc
1
(
s
1
)
γ
proc
2
(
s
2
)
P
.Fromthesemanticsof
γ
we obtain
N
→
⊆N
1
,and
P
=
P
1
γ
proc
2
(
s
2
),
(i)
∃
P
1
:
proc
1
(
s
1
)
P
1
,
N
N
→
∃
P
2
:
proc
2
(
s
2
)
P
2
,
N
⊆N
2
,and
P
=
proc
1
(
s
1
)
γ
P
2
,or,
(ii)
proc
1
(
s
1
)
N
1
proc
2
(
s
2
)
N
2
(iii)
∃
P
1
,P
2
,N
1
,N
2
:
→
1
P
1
,
→
2
P
2
,
N
=
N
1
|
γ
N
2
and
P
=
P
1
γ
P
2
.
By the definition of
proc
1
(
s
1
)and
proc
2
(
s
2
)wethenhave
g, t
1
:
s
1
N,g
⊆N
1
,and
P
=
(i)
∃
→
1
t
1
,
N
proc
1
(
t
1
)
γ
proc
2
(
s
2
),
g, t
2
:
s
2
N,g
∃
→
2
t
2
,
N
⊆N
2
,and
P
=
proc
1
(
s
1
)
γ
proc
2
(
t
2
), or,
(ii)
g
1
,g
2
,t
1
,t
2
,N
1
,N
2
:
s
1
N
1
,g
1
→
1
t
1
,
s
2
N
2
,g
2
(iii)
∃
→
2
t
2
,
N
=
N
1
|
γ
N
2
and
P
=
proc
1
(
t
1
)
γ
proc
2
(
t
2
).
N,g
→
N
→ proc
Therefore,
s
1
,s
2
t
1
,s
2
in
A
1
γ
A
2
,thus
proc
(
s
1
,s
2
)
(
t
1
,s
2
), while
proc
1
(
t
1
)
γ
proc
2
(
s
2
)
R proc
(
t
1
,s
2
) regarding (i). A symmetrical remark applies
N,g
→
N
→
regarding (ii). Finally,
s
1
,s
2
t
1
,t
2
with
g
=
γ
(
g
1
∧
g
2
),
proc
(
s
1
,s
2
)
proc
(
t
1
,t
2
), while
proc
1
(
t
1
)
γ
proc
2
(
t
2
)
R proc
(
t
1
,t
2
) regarding (iii).
