Information Technology Reference
In-Depth Information
Definition 4 (Hiding). The hiding of IMC
I
=( S,
Act
,
−→
,
,s 0 ) wrt. the
−→ ,
−→ is the
set A of actions is the IMC
I\
A =( S,
Act \
A,
,s 0 ) where
smallest relation defined by:
α
α
1. s
−−→
s and α
A implies s
−−→ s ,and
α
s and α
−−→
τ
s .
2. s
−−→
A implies s
Hiding thus transforms α -transitions with α
A into τ -transitions. All other
transition labels remain unaffected. This operation is of importance for the maxi-
mal progress assumption of IMCs. Turning an α -transition emanating from state
s ,say,intoa τ -transition may change the semantics of the IMC at hand, as after
hiding no Markovian transition will be ever taken in s .
Bisimulation. To compare IMCs, we introduce the notions of strong and weak
bisimulation. For set C
S of states and state s ,let R ( s, C )= s ∈C R ( s, s ).
Intuitively, two states s and t are strongly bisimilar if any interactive transition
s
α
−−→
α
−−→
t such that s and t are bisimilar. In
addition, the cumulative rate of moving from s to some equivalence class C of
states, i.e., R ( s, C )equals R ( t, C ). Since the probability of a Markovian transi-
tion to be executed immediately is zero, whereas internal interactive transitions
take always place immediately, there is no need to require equality of cumulative
rates if states have outgoing internal transitions. Let s
s can be mimicked by t , i.e., t
τ
−−→
/ denote a predicate
that is true if and only if s has no outgoing τ -transition. For state s ,action α
and C
s
α
s }
S ,let T ( s, α, C ) = 1 if and only if
{
C
|
s
−−→
is non-empty.
Definition 5 (Strong bisimulation). Let
I
=( S,
Act
,
−→
,
,s 0 ) be an
IMC. An equivalence relation R
S
×
S is a strong bisimulation on
I
if for
any ( s, t )
R and equivalence class C
S/R the following holds:
1. for any α
Act , T ( s, α, C )= T ( t, α, C ) ,and
τ
−−→
2. s
/
implies R ( s, C )= R ( t, C ) .
States s and s are strongly bisimilar, denoted s
s ,if ( s, s )
R for some
strong bisimulation R .
The rate equality is adopted from the notion of lumping equivalence [18]. Two
IMCs
I 1 and
I 2 on (disjoint) state spaces S 1 and S 2 respectively are bisimilar,
I 1 ∼I 2 , if there exists a strong bisimulation R on S 1
S 2 such that
denoted
( s 0 , 1 ,s 0 , 2 )
R . The next property asserts that
is substitutive with respect
I∼I implies for any set A that
to parallel composition and hiding, so, e.g.,
∼I
I\
A
\
A .
Theorem 1. [35]
is a congruence wrt. parallel composition and hiding.
As discussed before, τ -transitions play a special role in IMCs. Whereas strong
bisimulation treats all interactive transitions in the same way, regardless whether
they are internal (i.e., labelled by τ ) or not, weak bisimulation takes an ob-
server's point of view and cannot distinguish between executing several succes-
sive τ -transitions or a single one. This allows for collapsing sequences of internal
 
Search WWH ::




Custom Search