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