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

approximate ∼ by a binary relation R that is coarser than ∼ in general, and we check

† ʘ is invalid either and
MatchDistribution ( ʔ , ʘ ) returns false correctly. Otherwise, the two distributions
ʔ and ʘ are considered equivalent with respect to

† ʘ .If ʔ R † ʘ does not hold, then ʔ ∼

the validity of ʔ R

and we move on to match other
pairs of distributions. The correctness of the algorithm is stated in the following
theorem.

R

Theorem 3.14 Given two states s 0 , t 0 in a finitary pLTS, the function Bisim ( s 0 , t 0 )
terminates, and it returns true if and only if s 0 ∼ t 0 .

Proof Let Bis i stand for the i th execution of the function Bis . Let Assumed i and
NotBisim i be the set Assumed and NotBisim at the end of Bis i . When Bis i is
finished, either a WrongAssumption is raised or no WrongAssumption is raised.
In the former case, Assumed i ∩

; in the latter case, the execu-
tion of the function Bisim is completed. By examining function Close we see that
Assumed i ∩

NotBisim i =∅

NotBisim i − 1 =∅ . Now it follows from the fact NotBisim i − 1 ↆ NotBisim i

that NotBisim i − 1 ⊂ NotBisim i . Since we are considering finitary pLTSs, there is

some j such that NotBisim j − 1 = NotBisim j , when all the nonbisimilar state pairs

reachable from s 0 and t 0 have been found and Bisim must terminate.
For the correctness of the algorithm, we consider the relation

R i = Visited i − NotBisim i ,

where Visited i is the set Visited at the end of Bis i . Let Bis k be the last execution
of Bis . For each i

≤ k , the relation R i can be regarded as an approximation of

∼ R i is a coarser

approximation because if two states s , t are revisited but their relation is unknown,
they are assumed to be bisimilar. Therefore, if Bis k ( s 0 , t 0 ) returns false , then s 0 ∼

, as far as the states appeared in R i are concerned. Moreover,

t 0 .

On the other hand, if Bis k ( s 0 , t 0 ) returns true , then R k constitutes a bisimulation

relation containing the pair ( s 0 , t 0 ). This follows because Match ( s 0 , t 0 )

= true ,

a
−ₒ ʔ there exists some transition which basically means that whenever s R k t and s

a
−ₒ R k † ʘ . Indeed, this rules out

t ʘ such that Check ( ʔ , ʘ , R k ) = true , i.e. ʔ

the possibility that s 0 ∼ t 0 as otherwise we would have s 0 ∼ ˉ t 0 by Proposition 3.8 ,

that is s 0 ∼ n t 0 for some n> 0. The latter means that some transition s 0

a
−ₒ

ʔ

a
−ₒ ∼ n − 1 ) † ʘ , or symmetrically

with the roles of s 0 and t 0 exchanged, i.e. ʔ and ʘ can be distinguished at level n ,
so a contradiction arises.
Below we consider the time and space complexities of the algorithm.

exists such that for all t 0 ʘ we do not have ʔ (

Theorem 3.15 Let s and t be two states in a pLTS with n states in total. The function
Bisim ( s , t ) terminates in time O ( n 7 / log n ) and space O ( n 2 ) .
Proof The number of state pairs is bounded by n 2 . In the worst case, each execution
of the function Bis ( s , t ) only yields one new pair of states that are not bisimilar. The
number of state pairs examined in the first execution of Bis ( s , t ) is at most O ( n 2 ), in
the second execution is at most O ( n 2 − 1), ... . Therefore, the total number of state

pairs examined is at most O ( n 2 + ( n 2 − 1) +···+ 1) = O ( n 4 ). When a state pair ( s , t )