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

distributions rather than on states. Another notion of distribution-based bisimula-
tion is given in [ 74 ]. Unlike the other bisimulations we have discussed so far, it is
essentially a linear-time semantics rather than a branching-time semantics [ 75 ].
The Kantorovich metric has been used by van Breugel et al. for defining be-
havioural pseudometrics on fully probabilistic systems [ 40 , 76 , 77 ] and reactive
probabilistic systems [ 55 , 78 - 80 ]; and by Desharnais et al. for labelled Markov
chains [ 81 , 57 ] and labelled concurrent Markov chains [ 56 ]; and later on by Ferns
et al. for Markov decision processes [ 82 , 83 ]; and by Deng et al. for action-labelled
quantitative transition systems [ 84 ]. In this chapter we are mainly interested in the
correspondence of our lifting operation to the Kantorovich metric. The metric char-
acterisation of probabilistic bisimulation in Sect. 3.7 is merely a direct consequence
of this correspondence. In [ 85 ] a general family of bisimulation metrics is proposed,
which can be used to specify some properties in security and privacy. In [ 86 ] a differ-
ent kind of approximate reasoning technique is proposed that measures the distances
of labels used in (nonprobabilistic) bisimulation games rather than the distances of
states in probabilistic bisimulation games.
Decision algorithms for probabilistic bisimilarity and similarity are first investi-
gated by Baier et al. in [ 26 ]. In [ 87 ] Zhang et al. have improved the original algorithm
of computing probabilistic simulation by exploiting the parametric maximum flow
algorithm [ 88 ] to compute the maximum flows of networks and resulted in an algo-
rithm that computes strong simulation in time

( m 2 ). In [ 89 ]
a framework based on abstract interpretation [ 90 ] is proposed to design algorithms
that compute bisimulation and simulation. It entails the bisimulation algorithm by
Baier et al. as an instance and leads to a simulation algorithm that improves the one
for pLTSs by Zhang et al. All those algorithms above are global in the sense that
a whole state space has to be fully generated in advance. In contrast, “on-the-fly”
algorithms are local in the sense that the state space is dynamically generated, which
is often more efficient to determine that one state fails to be related to another. Our
algorithm in Sect. 3.8.2 is inspired by [ 26 ] because we also reduce the problem of
checking whether two distributions are related by a lifted relation to the maximum
flow problem of a suitable network. We generalise the local algorithm of checking
nonprobabilistic bisimilarity [ 61 , 62 ] to the probabilistic setting.
An important line of research is on denotational semantics of probabilistic pro-
cesses, where bisimulations are interpreted in analytic spaces. This topic is well
covered in [ 50 , 91 ], and thus omitted from this topic.

O ( m 2 n ) and in space O

References

1. Giacalone, A., Jou, C.C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent sys-
tems. Proceedings of IFIP TC2 Working Conference on Programming Concepts and Methods,
Sea of Galilee, Israel (1990)
2. Christoff, I.: Testing equivalences and fully abstract models for probabilistic processes.
Proceedings of the 1st International Conference on Concurrency Theory. Lecture Notes in
Computer Science, vol. 458, pp. 126-140. Springer, Heidelberg (1990)