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

˄

1/3

˄

2/3 1/ 3 2/ 3

˄ a

a

1/3 2/3

a

˄

(a) (b)

Fig. 3.1 Example pLTSs

are labelled with positive real numbers that sum to 1. Sometimes we partially unfold
this graph by drawing the same nodes multiple times; in doing so, all outgoing edges
of a given instance of a node are always drawn, but not necessarily all incoming
edges. Edges labelled by probability 1 occur so frequently that it makes sense to
omit them, together with the associated nodes

representing point distributions.
Two example pLTSs are described this way in Fig. 3.1 , where part (b) depicts the
initial part of the pLTS obtained by unfolding the one in part (a).
For each state s , the outgoing transitions s ʱ

ⓦ

−ₒ ʔ represent the nondeterministic
alternatives available in the state s . The nondeterministic choices provided by s are
supposed to be resolved by the environment, which is formalised by a scheduler or an
adversary . On the other hand, the probabilistic choices in the underlying distribution
ʔ are made by the system itself. Therefore, for each state s , the environment chooses
some outgoing transition s

ʱ
−ₒ ʔ . Then the action ʱ is performed, the system

resolves the probabilistic choice, and subsequently with probability ʔ ( s ) the system
reaches state s .
If we impose the constraint that for any state s and action ʱ at most one outgoing
transition from s is labelled ʱ , then we obtain the special class of pLTSs called re-
active (or deterministic ) pLTSs that are the probabilistic counterpart to deterministic
LTSs. Formally, a pLTS is reactive if for each s

ʱ
−ₒ ∈ S , ʱ ∈ L we have that s ʔ

ʱ
−ₒ ʔ imply ʔ = ʔ .

and s