Information Technology Reference
In-Depth Information
=
definition of Con
Hr (( T ( P ); term
SKIP )
| S Con |
C ([[ ]]))
=
reduction of parallel composition: C ([[ ]]) never refuses x : S Con
SKIP ) .
Hr ( T ( P ); term
=
term ∈ H Hr
Hr ( T ( P )) .
The exposition of hidden transitions is important from a practical point of view
because it allows the assignment of user-defined functions to computations that
are (although present) not observable from outside the computing system, en-
abling the determination of events concurrent with those hidden transitions. On
the theoretical side, this decision restricts equality of the source process P with
its extended version Ext ( P ) to the traces model because hiding does not dis-
tribute over external choice if initial events are affected. Neither does hiding
distribute over parallel composition if the hidden alphabet intersects with the
synchronization set. The following lemma shows that parallel e events can safely
be removed from the synchronization sets in T so that the two sets no longer
intersect, and distributivity of hiding over parallel composition holds in T .
Lemma 2.
Writing A =
and A =
{
s . x , e . x
|
x
A
}
{
s . x
|
x
A
}
,
Hr ( T ( P )
| A |
T ( Q )) = Hr ( T ( P )
| A |
T ( Q )) .
Proof. The proof follows by s-e-precedence (1), e-non-refusability (2) and s-e-
conflict-freedom (3).
Firstly, the equality holds trivially if A =
.By(1),any
e . x event is preceded by (a not necessarily adjacent) s . x event; thus we focus on
s events. Since the result does not affect x /
; thus assume A
=
A , we can further restrict attention
to s . x , x : A . Thus assume s . x , x : A have occurred on both sides. By definition
of T , neither side can refuse s . y , ( x , y )
conc ( P
| A |
Q ). So assume both sides
} . By proposition 2, neither side can refuse any
have performed t :
{
s . x
|
x
A
of e . x , s . x
in t is refused. Furthermore,
by proposition 3, no e . x event conflicts with any of the subsequent s events.
Thus, synchronizing on e . x , x : A does not affect subsequent s events.
t , whilst by proposition 1, any e . x , s . x
Finiteness of P is not required in the proof. One might suspect that hiding of
e events might introduce divergence, but this could happen only if there were
unbounded sequences of e events. Such sequences could be introduced by a cycle
of e events but the construction of T prevents cycles of e events. Furthermore,
processes such as μ P
P ), although infinite state, cannot perform
unbounded sequences of e events either. The s-e-precedence property asserts that
each infinite sequence of e events must be preceded by an infinite sequence of
s events. But unbounded sequences of s events would prevent the occurrence
of any e event; so whenever e events are observable there cannot have been
unbounded sequences of s events in T ( P ); so divergence cannot occur.
·
( x
SKIP
| |
 
Search WWH ::




Custom Search