Information Technology Reference
In-Depth Information
7.3
Compositionality
The main operator of interest in modelling concurrent systems is the parallel com-
position. We will use a parallel composition from the calculus of communicating
systems (CCS)
. It is convenient for the proofs in Sect.
7.4
, so we add it to our
language
rpCSP
presented in Sect. 6.2. Its behaviour is specified by the following
three rules.
|
ʱ
−ₒ
ʱ
−ₒ
s
1
ʔ
s
2
ʔ
ʱ
−ₒ
ʱ
−ₒ
s
1
|
s
2
ʔ
|
s
2
s
1
|
s
2
s
1
|
ʔ
a
−ₒ
a
−ₒ
s
1
ʔ
1
,
s
2
ʔ
2
.
˄
−ₒ
s
1
|
ʔ
1
|
s
2
ʔ
2
Intuitively in the parallel composition of two processes, each of them can proceed in-
dependently or synchronise on any visible action they share with each other. The rules
use the obvious extension of the function
|
on pairs of states to pairs of distributions.
To be precise
ʔ
|
ʘ
is the distribution defined by:
ʔ
(
s
1
)
·
ʘ
(
s
2
)i
s
=
s
1
|
s
2
(
ʔ
|
ʘ
)(
s
)
=
0
otherwise
This construction can also be explained as follows:
Lemma 7.1
For any state t and distributions ʔ
,
ʘ,
ʔ
|
t
=
s
∈
ʔ
ʔ
(
s
)
(i)
·
(
s
|
t
)
ʔ
|
ʘ
=
t
∈
ʘ
ʘ
(
t
)
(ii)
·
(
ʔ
|
t
).
Proof
Straightforward calculation.
are closed under the parallel composition. This
requires some preliminary results, particularly on composing actions from the
components of a parallel composition, as in Lemma 6.27.
We show that both
≈
s
and
≈
Lemma 7.2
In a pLTS,
ʱ
−ₒ
ʱ
−ₒ
ʔ
implies ʔ
ʔ
|
(i)
ʔ
|
ʘ
ʘ
,
for ʱ
∈
Act
˄
a
−ₒ
a
−ₒ
˄
−ₒ
ʔ
1
ʔ
2
ʔ
1
|
ʔ
2
,
for a
(ii)
ʔ
1
and ʔ
2
implies ʔ
1
|
ʔ
2
∈
Act
.
Proof
Each case follows by straightforward linearity arguments. As an example, we
outline the proof of (i).
ʔ
ʱ
−ₒ
ʔ
means that
ʱ
−ₒ
ʔ
=
ʔ
=
p
i
·
s
i
s
i
ʔ
i
p
i
·
ʔ
i
i
∈
I
i
∈
I
ʱ
−ₒ
ʔ
i
|
t
. By linearity we can immediately infer that
For any state
t
,
wehave
s
i
|
t
i
∈
I
p
i
·
−ₒ
i
∈
I
p
i
·
ʱ
(
s
i
|
t
)
(
ʔ
i
|
t
) and this may be rendered as
ʱ
−ₒ
ʔ
|
t
ʔ
|
t
Search WWH ::
Custom Search