Probabilistic Bisimulation - Semantics of Probabilistic Processes: An Operational Approach - page 45

L hm is adequate with respect to probabilistic bisimilarity.
Theorem 3.7 (Adequacy) Let s and t be any two states in a finite-state pLTS. Then
s

It turns out that

= L hm t. ∼ t if and only if s

Proof ( ⃒ ) Suppose s ∼ t . We show that s |= ˕ ⃔ t |= ˕ by structural induction

on ˕ .

• Let s |= . Then we clearly have t |= .

• Let s |= ˕ 1 ∧ ˕ 2 . Then s |= ˕ i for i = 1, 2. So by induction t |= ˕ i , and we have

t |= ˕ 1 ∧ ˕ 2 . By symmetry we also have t |= ˕ 1 ∧ ˕ 2 implies s |= ˕ 1 ∧ ˕ 2 .

• Let s |= ¬ ˕ .So s |= ˕ , and by induction we have t |= ˕ . Thus t |= ¬ ˕ .By

symmetry we also have t |= ˕ implies s |= ˕ .

a
−ₒ

|= |=

• Let s a ( ˕ 1 p ↕ ˕ 2 ). Then s ʔ and ʔ ˕ 1 p ↕ ˕ 2 for some ʔ .Sowehave

1, 2 and s ∈ we have s |=

ʔ = p · ʔ 1 + (1 − p ) · ʔ 2 and for all i = ʔ i ˕ i .

a
−ₒ

†

Since s ∼ t , there is some ʘ with t ʘ and ʔ ∼ ʘ . By Proposition 3.3

† ʘ i for i

we have that ʘ = p · ʘ 1 + (1 − p ) · ʘ 2 and ʔ i ∼ = 1, 2. It follows

that for each t ∈ there is some s ∈ with s ∼ t . So by induction we

ʘ i ʔ i

have t |= ˕ i for all t ∈

ʘ i with i = 1, 2. Therefore, we have ʘ |= ˕ 1 p ↕ ˕ 2 .

It follows that t |= a ( ˕ 1 p ↕ ˕ 2 ). By symmetry we also have t |= a ( ˕ 1 p ↕ ˕ 2 )

implies s |= a ( ˕ 1 p ↕ ˕ 2 ).

= L hm = L hm

( ⃐ ) We show that the relation is a probabilistic bisimulation. Obviously

={

U i |

∈ }

is an equivalence relation. Let E i I be the set of all equivalence classes

= L hm . We first claim that, for any equivalence class U i , there exists a formula ˕ i
satisfying [[ ˕ i ]]

of

U i . This can be proved as follows:
• f E contains only one equivalence class U 1 , then U 1 = S . So we can take the
required formula to be

=

= S .
• f E contains more than one equivalence class, then for any i , j ∈ I with i = j ,
there exists a formula ˕ ij such that s i |=

because [[ ]]

˕ ij and s j |= ˕ ij for any s i ∈ U i and

s j ∈ U j . Otherwise, for any formula ˕ , s i |= ˕ implies s j |= ˕ . Since the negation

exists in the logic L hm , we also have s i |= ¬ ˕ implies s j |= ¬ ˕ , which means

s j |= ∈ L hm , which

contradicts the fact that s i and s j are taken from different equivalence classes. For
each index i

˕ implies s i |= ˕ . Then s i |= ˕ ⃔ s j |= ˕ for any ˕

I , define ˕ i = j = i ˕ ij , then by construction [[ ˕ i ]] ∈ = U i . Let us

check the last equality. On one hand, if s ∈ [[ ˕ i ]], then s |=

˕ i which means that

s |= i . That is, s ∈

˕ ij for all j = U j for all j = i , and this in turn implies that

s ∈ U i . On the other hand, if s ∈ U i then s |=

˕ i as s i |= ˕ i , which means that

s ∈ [[ ˕ i ]] .

This completes the proof of the claim that for each equivalence U i we can find a
formula ˕ i with [[ ˕ i ]] = U i .

a
−ₒ = L hm

Now let s t and s ʔ . By Theorem 3.1 (2) it remains to show that

a
−ₒ t ʘ for some ʘ with

= ∈

ʔ ( U i ) ʘ ( U i ) for any i I. (3.16)