Information Technology Reference
In-Depth Information
For general choice, T splits each event x into its start event s . x and end event
e . x . As special cases,
T ( P )= STOP
T ( SKIP )= SKIP
T ( x
P )= s . x
e . x
T ( P ) .
T distributes over sequential composition, external choice and parallel composi-
tion, in the latter case by synchronizing on the split events instead of the original
events. For hiding, T communicates the split events over the channels sh and
eh (standing for 'start hidden' and 'end hidden', respectively). For each internal
choice, thought of as resulting from an internal transition, T introduces a fresh
hidden event labelled ic i for that transition. It is then split and communicated
over the sh and eh channels responsible for hidden events. T distributes over
renaming by lifting the renaming to the split events. Finally T distributes over
the operands of a timeout, replaces the timeout by external choice and intro-
duces a fresh timeout event labelled to i for each timeout communicated over
the channels sh and eh responsible for hidden events (recall the motivation for
the timeout operator to express the abstraction of one initial event in an external
choice; see, for example, [9]).
The alphabets of P and T ( P )aredisjoint,since
Σ T ( P ) ⊆{|
s , e , sh , eh
|}
.
Equality (in the traces model) with the original process P is established by hiding
the end events of the original visible transitions and all events corresponding to
hidden transitions and renaming the start events of the original transition back
to their source names. The exposition of hidden transitions disallows equality in
the failures (and in the failures-divergences) model, because in general
( P
Q )
\
A
= P
\
A
Q
\
A
in these models, but
( P
Q )
\
A = T
P
\
A
Q
\
A .
Thus, there is no construction F using parallel composition, hiding and renaming
such that F ( T ( P
Q . In the next section we present a construc-
tion that preserves the traces of the original process and reveals its internal
concurrency.
Q )) = P
4 Assembling the System
The 'control process' to be placed in parallel with a transformed process is
defined in terms of a parameter X denoting a bag; bag union is denoted
,bag
difference
, and bag comprehension is written [[ x 0 ,..., x n ]]. Initially the bag is
 
Search WWH ::




Custom Search