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

nondeterministic and reactive probabilistic choices is proposed in [ 4 ]. It is slightly
reformulated in [ 6 ] under the name simple probabilistic automata , which is akin to
our pLTS model. Note that essentially the same model has appeared in the litera-
ture under different names such as NP-systems [ 69 ], probabilistic processes [ 70 ],
probabilistic transition systems [ 14 ] etc. Furthermore, there are strong structural
similarities with Markov decision processes [ 71 ].
Following the classification above, our model is reactive rather than generative.
The reactive model of [ 23 ] can be reformulated by saying that a state s has at most
one outgoing transition for any action a , and this transition ends in a probability
distribution over its successor states. The generalisation of [ 6 ], that we use here as
well, is that a state can have multiple outgoing transitions with the same label, each
ending in a probability distribution. Simple probabilistic automata are a special case
of the probabilistic automata of [ 6 ], that also generalise the generative models of
probabilistic processes to a setting with nondeterministic choice.

3.9.2 Probabilistic Bisimulation

Probabilistic bisimulation was first introduced by Larsen and Skou [ 23 ]. Later on,
it has been investigated in a great many probabilistic models. An adequate logic
for probabilistic bisimulation in a setting similar to our pLTSs has been studied in
[ 45 , 47 ] and then used in [ 72 ] to characterise a notion of bisimulation defined on an
LTS whose states are distributions. It is also based on a probabilistic extension of
the Hennessy-Milner logic. The main difference from our logic in Sect. 3.6.1 is the
introduction of the operator [

] p . Intuitively, a distribution ʔ satisfies the formula
[ ˕ ] p when the set of states satisfying ˕ is measured by ʔ with probability at least
p . So the formula [ ˕ ] p can be expressed by our logic in terms of the probabilistic
choice ˕ p ↕

·

, as we have seen in Example 3.1 .
An expressive logic for nonprobabilistic bisimulation has been proposed in [ 53 ]. In
Sect. 3.6.2 we partially extend the results of [ 53 ] to a probabilistic setting that admits
both probabilistic and nondeterministic choice. We present a probabilistic extension
of the modal mu-calculus [ 31 ], where a formula is interpreted as the set of states
satisfying it. This is in contrast to the probabilistic semantics of the mu-calculus as
studied in [ 11 , 12 , 18 ] where formulae denote lower bounds of probabilistic evidence
of properties, and the semantics of the generalised probabilistic logic of [ 16 ] where
a mu-calculus formula is interpreted as a set of deterministic trees that satisfy it.
The probabilistic bisimulation studied in this chapter (cf. Definition 3.5 ) is a rela-
tion between states. In [ 73 ] a notion of probabilistic bisimulation is directly defined
on distributions, and it is shown that the distribution-based bisimulations correspond
to a lifting of state-based bisimulations with combined transitions. By combined tran-
sitions we mean that if a state can perform an action and then nondeterministically
evolve into two different distributions, it can also evolve into any linear combina-
tion of the two distributions. The logical characterisation of the distribution-based
bisimilarity in [ 73 ] is similar to ours in Sect. 3.6.1 but formulae are interpreted on