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

Let

˕ : = a ( ˕ ip i ↕ )

i ∈ I

where p i = ʔ ([[ ˕ i ]]). It is easy to see that s |= ˕ , which implies that t |= ˕ .

|= i ∈ I ( ˕ ip i ↕

a
−ₒ Therefore, there exists a distribution ʘ with t ʘ and ʘ ).

Then for each i ∈ I we have ʘ |= ˕ ip i ↕ , implying that ʘ ( U i ) = ʘ ([[ ˕ i ]] ) ≥

ʔ ( U i ). Note that i ∈ I p i = p i =

= =

ʔ ([[ ˕ i ]] ) 1. Thus we have ʔ ( U i ) ʘ ( U i ) for

∈

each i I , the goal set in ( 3.16 ).

By symmetry each transition of t can be matched by some transition of s .

The above theorem still holds if the pLTS has a countable state space but is
image-finite. The proof is a bit subtle; see [ 45 ] for more details.
When restricted to reactive pLTSs, probabilistic bisimulations can be charac-
terised by simpler forms of logics [ 23 , 46 , 47 ] or a simple test language [ 48 ]. Most
notably, in the absence of nondeterminism, there is no need of negation to characterise
probabilistic bisimulations.
Let us fix a reactive pLTS S , L , ₒ where the state space S may be countable.

Let L rhm be the sublogic of L hm generated by the following grammar:

˕ : =| ˕ 1 ∧ ˕ 2 | a ( ˕ 1 p ↕ )

where p is a rational number in the unit interval [0, 1]. Recall that s |= a ( ˕ p ↕ )

a
−ₒ iff s ʔ and ʔ ([[ ˕ ]] ) ≥ p (cf. Example 3.1 ). The logic above induces a logical

= L rhm between states.
The following lemma says that the transition probabilities to sets of the form [[ ˕ ]]
are completely determined by the formulae. It has appeared as Lemma 7.7.6 in [ 49 ].

equivalence relation

a
−ₒ

a
−ₒ = L rhm t and s

Lemma 3.4 If s ʔ, then some ʘ exists with t ʘ, and for

any formula ˕ ∈ L rhm we have ʔ ([[ ˕ ]] ) = ʘ ([[ ˕ ]] ) .

Proof First of all, the existence of ʘ is obvious because otherwise the formula

a ) would be satisfied by s but not by t .

Let us assume, without loss of generality, that there exists a formula ˕ such
that ʔ ([[ ˕ ]] ) <ʘ ([[ ˕ ]]). Then we can always squeeze in a rational number p with
ʔ ([[ ˕ ]] ) <p

( 1 ↕

≤ ʘ ([[ ˕ ]]). It follows that t |= a ( ˕ p ↕ )but s |= a ( ˕ p ↕ ),

= L rhm t . which contradicts the hypothesis that s

L rhm can characterise bisimulation for reactive pLTSs.
The completeness proof of the characterisation crucially relies on the ˀ - ʻ theorem
(cf. Theorem 2.9). The next proposition is a typical application of that theorem [ 50 ],
which tells us that when two probability distributions agree on a ˀ -class they also
agree on the generated ˃ -algebra.

We will show that the logic

Proposition 3.9 Let A 0 ={ [[ ˕ ]] | ˕ ∈ L rhm } and A = ˃ ( A 0 ) . For any two

distributions ʔ , ʘ ∈ D ( S ) ,ifʔ ( A ) = ʘ ( A ) for any A ∈ A 0 , then ʔ ( B ) = ʘ ( B )

for any B ∈ A .