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

is examined, each transition of s is compared with all transitions of t labelled with
the same action. Since the pLTS is finitely branching, we could assume that each
state has at most c outgoing transitions. Therefore, for each state pair, the number of
comparisons of transitions is bound by c 2 . As a comparison of two transitions calls
the function Check once, which requires time O ( n 3 / log n ) by Lemma 3.10 .Asa
result, examining each state pair takes time O ( c 2 n 3 / log n ).
Finally, the worst case time complexity of executing Bisim ( s , t )is O ( n 7 / log n ).
The space requirement of the algorithm is easily seen to be O ( n 2 ), in view of
Lemma 3.10 .

Remark 3.3 With mild modification, the above algorithm can be adapted to check
probabilistic similarity. We simply remove the underlined part in the function
MatchAction ; the rest of the algorithm remains unchanged. Similar to the analysis
in Theorems 3.14 and 3.15 , the new algorithm can be shown to correctly check prob-
abilistic similarity over finitary pLTSs; its worst case time and space complexities
are still O ( n 7 / log n ) and O ( n 2 ), respectively.

3.9 Bibliographic Notes

3.9.1 Probabilistic Models

Models for probabilistic concurrent systems have been studied for a long time [ 64 -
67 ]. One of the first models obtained as a simple adaptation of the traditional LTSs
from concurrency theory appears in [ 23 ]. Their probabilistic transition systems are
classical LTSs, where in addition every transition is labelled with a probability, a
real number in the interval [0,1], such that for every state s and every action a , the
probabilities of all a -labelled transitions leaving s sum to either 0 or 1.
In [ 1 ] a similar model is proposed, but where the probabilities of all transitions
leaving s sum to either 0 or 1. Van Glabbeek et al. [ 68 ] propose the terminology
reactive for the type of model studied in [ 23 ], and generative for the type of model
studied in [ 1 ]. In a generative model, a process can be considered to spontaneously
generate actions, unless restricted by the environment; in generating actions, a prob-
abilistic choice is made between all transitions that can be taken from a given state,
even if they have different labels. In a reactive model, on the other hand, processes
are supposed to perform actions only in response to requests by the environment.
The choice between two different actions is therefore not under the control of the
process itself. When the environment requests a specific action, a probabilistic choice
is made between all transitions (if any) that are labelled with the requested action.
In the aforementioned models, the nondeterministic choice that can be modelled
by nonprobabilistic LTSs is replaced by a probabilistic choice (and in the genera-
tive model also a deterministic choice, a choice between different actions, is made
probabilistic). Hence reactive and generative probabilistic transition systems do not
generalise nonprobabilistic LTSs. A model, or rather a calculus, which features both