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

Fig. 3.9 Computing bisimulation equivalence classes in pLTSs

† ʘ , for two given distributions ʔ , ʘ and a relation

for deciding whether ʔ R R .We

construct the network ) and compute the maximum flow with well-known

methods, as sketched in the procedure Check shown in Fig. 3.10 .
As shown in [ 60 ], computing the maximum flow in a network can be done in time
O ( n 3 / log n ) and space O ( n 2 ), where n is the number of nodes in the network. So
we immediately have the following result.

N ( ʔ , ʘ , R

† ʘ can be done in time O ( n 3 / log n ) and space

Lemma 3.10 The test whether ʔ R

O ( n 2 ) .

We now present a bisimilarity-checking algorithm by adapting the algorithm
proposed in [ 61 ] for value-passing processes, which in turn was inspired by [ 62 ].
The main procedure in the algorithm is Bisim ( s , t ) shown in Fig. 3.10 . It starts with
the initial state pair ( s , t ), trying to find the smallest bisimulation relation containing
the pair by matching transitions from each pair of states it reaches. It uses three
auxiliary data structures:

• NotBisim collects all state pairs that have already been detected as not bisimilar.

• Visited collects all state pairs that have already been visited.

• Assumed collects all state pairs that have already been visited and assumed to be

bisimilar.

The core procedure, Match , is called from function Bis inside the main procedure
Bisim . Whenever a new pair of states is encountered it is inserted into Visited .If
two states fail to match each other's transitions then they are not bisimilar and the
pair is added to NotBisim . If the current state pair has been visited before, we check
whether it is in NotBisim . If this is the case, we return false . Otherwise, a loop has
been detected and we make assumption that the two states are bisimilar, by inserting
the pair into Assumed , and return true . Later on, if we find that the two states are not
bisimilar after finishing searching the loop, then the assumption is wrong, so we first
add the pair into NotBisim and then raise the exception WrongAssumption , which
forces the function Bis to run again, with the new information that the two states
in this pair are not bisimilar. In this case, the size of NotBisim has been increased
by at least one. Hence, Bis can only be called for finitely many times. Therefore,
the procedure Bisim ( s , t ) will terminate. If it returns true , then the set of state pairs
(Visited - NotBisim) constitutes a bisimulation relation containing the pair ( s , t ).
The main difference from the algorithm of checking nonprobabilistic bisimilarity
in [ 61 ] is the introduction of the procedure MatchDistribution ( ʔ , ʘ ), where we