Information Technology Reference
In-Depth Information
names
γ
−
1
[
N
1
]=
γ
−
2
[
N
2
]. Also, for a constraint
g
,wewrite
γ
(
g
) for the for-
mula obtained by replacing port names in
γ
1
[
N
]
⊆N
1
and
γ
2
[
N
]
⊆N
2
by the
corresponding name in
N
.
Definition 3.
For two constraint automata
A
1
and
A
2
with port synchroniza-
tion function
γ
, the constraint automaton
A
1
γ
A
2
, called the
γ
-synchronous
N
,
s
0
,s
0
product of
A
1
and
A
2
, is given by
A
1
γ
A
2
=(
S
1
×
S
2
,
→
,
)
where
N
=
N
1
|
γ
N
2
and the transition relation
→
is determined by the following rules:
s
1
N
1
,g
1
s
2
N
2
,g
2
N
1
⊆N
1
N
2
⊆N
2
−−−−→
1
t
1
−−−−→
1
t
2
(3)
N
1
,g
1
−−−−→
N
2
,g
2
−−−−→
s
1
,s
2
t
1
,s
2
s
1
,s
2
s
1
,t
2
and
s
1
N
1
,g
1
s
2
N
2
,g
2
γ
−
1
1
(
N
1
)=
γ
−
1
2
−−−−→
1
t
1
−−−−→
1
t
2
(
N
2
)
(4)
N
1
|
γ
N
2
,γ
(
g
1
∧g
2
)
−−−−−−−−−−−→
s
1
,s
2
t
1
,t
2
In the above setting, for a port
n
∈N
, the idea is that the ports
n
1
=
γ
1
(
n
)
∈N
1
and
n
2
=
γ
2
(
n
)
∈N
2
synchronize. Thus, either
n
1
and
n
2
have both flow or
n
1
and
n
2
have both no flow, expressed as
n
having flow or no flow, respectively. The
resulting automaton, the so-called synchronized product automaton
A
1
γ
A
2
,
follows the flow of
A
1
and
A
2
, based on the first two rules for the transition
relation, but requires the flow on its ports in
N
to be agreed upon by
A
1
and
A
2
.
P
2
in
mCRL2
, being based on the process alge-
bra ACP [10], has its transitions derived from the steps of its left component
P
1
,
its right component
P
2
, or their synchronization:
A parallel composition
P
1
P
1
P
2
=
P
1
P
2
+
P
2
P
1
+
P
1
|
P
2
Here,
denotes the left merge, an auxiliary operator in
mCRL2
.Giventwopro-
cesses
p
and
q
, the left merge, written
p
q
,requires
p
to execute an action first
and thereafter continues as the parallel composition of the remainder of
p
and
q
.
In the context of the synchronization product
A
1
γ
A
2
of constraint au-
tomata two aspects are important. Firstly, the port synchronization function
γ
decides which ports synchronize, hence which sets of port names are non-trivially
combined. For example, (
a
Q
)if
γ
(
a, b
)=
c
.Ifnot
stated otherwise, the communication operator is assumed to yield the inaction
δ
.
Secondly, ports that are to be synchronized, i.e.
γ
1
[
N
]
·
Q
)
|
(
b
·
Q
) yields
c
·
(
Q
⊆N
2
,
have their names erased from the alphabet. Thus, for the first issue, we define
the attributes of the
mCRL2
communication operator for a parallel composition as
determined by a port synchronization for the synchronized product of two con-
straint automata. For the second issue, we will apply a specific blocking operator
determined by the port synchronization.
⊆N
1
and
γ
2
[
N
]
Definition 4.
Given a port synchronization function
γ
with mappings
γ
1
:
N→
N
1
,
γ
2
:
process
P
1
γ
P
2
, called the
γ
-synchronized merge
of
P
1
and
P
2
,isdefinedasfollows:
N→N
2
,the
mCRL2
P
1
γ
P
2
=
∂
B
(
Γ
C
(
P
1
P
2
))
