=Paper=
{{Paper
|id=Vol-1720/full15
|storemode=property
|title=Disjunctive Probabilistic Modal Logic is Enough for
Bisimilarity on Reactive Probabilistic Systems
|pdfUrl=https://ceur-ws.org/Vol-1720/full15.pdf
|volume=Vol-1720
|authors=Marco Bernardo,Marino Miculan
|dblpUrl=https://dblp.org/rec/conf/ictcs/BernardoM16
}}
==Disjunctive Probabilistic Modal Logic is Enough for
Bisimilarity on Reactive Probabilistic Systems==
https://ceur-ws.org/Vol-1720/full15.pdf
Disjunctive Probabilistic Modal Logic is Enough
for Bisimilarity on Reactive Probabilistic Systems
Marco Bernardo1 and Marino Miculan2
1
Dip. di Scienze Pure e Applicate, Università di Urbino, Italy
2
Dip. di Scienze Matematiche, Informatiche e Fisiche, Università di Udine, Italy
Abstract. Larsen and Skou characterized probabilistic bisimilarity over
reactive probabilistic systems with a logic including true, negation, con-
junction, and a diamond modality decorated with a probabilistic lower
bound. Later on, Desharnais, Edalat, and Panangaden showed that nega-
tion is not necessary to characterize the same equivalence. In this paper,
we prove that the logical characterization holds also when conjunction is
replaced by disjunction, with negation still being not necessary. To this
end, we introduce reactive probabilistic trees, a fully abstract model for re-
active probabilistic systems that allows us to demonstrate expressiveness
of the disjunctive probabilistic modal logic, as well as of the previously
mentioned logics, by means of a compactness argument.
1 Introduction
Since its introduction [12], probabilistic bisimilarity has been used to compare
probabilistic systems. It corresponds to Milner’s strong bisimilarity for nonde-
terministic systems, and coincides with lumpability for Markov chains. Larsen
and Skou [12] first proved that bisimilarity for reactive probabilistic systems can
be given a logical characterization: two processes are bisimilar if and only if
they satisfy the same set of formulas of a propositional modal logic similar to
Hennessy-Milner logic [10]. In addition to the usual constructs >, ¬, and ∧, this
logic features a diamond modality haip φ, which is satisfied by a state if, after
performing action a, the probability of being in a state satisfying φ is at least p.
Later on, Desharnais, Edalat, and Panangaden [6] showed that negation is
not necessary for discrimination purposes, by working in a continuous-state
setting. This result has no counterpart in the nonprobabilistic setting, where
Hennessy-Milner logic without negation characterizes simulation equivalence,
which is strictly coarser than bisimilarity [8] (while the two equivalences are
known to coincide on reactive probabilistic systems [2]).
Copyright c by the paper’s authors. Copying permitted for private and academic pur-
poses.
V. Biló, A. Caruso (Eds.): ICTCS 2016, Proceedings of the 17th Italian Conference on
Theoretical Computer Science, 73100 Lecce, Italy, September 7–9 2016, pp. 203–217
published in CEUR Workshop Proceedins Vol-1720 at http://ceur-ws.org/Vol-1720
204 M. Bernardo, M. Miculan
In this paper, we show that ∨ can be used in place of ∧ without having to
reintroduce negation: the constructs >, ∨, and haip suffice to characterize bisim-
ilarity on reactive probabilistic systems. The intuition is that from a conjunctive
distinguishing formula we can often derive a disjunctive one by suitably increas-
ing some probabilistic lower bounds. Not even this result has a counterpart in
the nonprobabilistic setting, where replacing conjunction with disjunction in the
absence of negation yields trace equivalence (this equivalence does not coincide
with bisimilarity on reactive probabilistic processes).
The proof of our result relies on a simple categorical construction of a seman-
tics for reactive probabilistic systems, which we call reactive probabilistic trees
(Sect. 3). This semantics is fully abstract, i.e., two states are probabilistically
bisimilar if and only if they are mapped to the same reactive probabilistic tree.
Moreover, the semantics is compact, in the sense that two (possibly infinite) trees
are equal if and only if all of their finite approximations are equal. Hence, in
order to prove that a logic characterizes probabilistic bisimilarity, it suffices to
prove that it allows to discriminate finite reactive probabilistic trees. Indeed,
given two different finite trees, we can construct a formula of the considered logic
(by induction on the height of one of the trees) that tells the two trees apart and
has a depth not exceeding the height of the two trees (Sect. 4). Our technique
applies also to the logics in [12,6], for which it allows us to provide simpler proofs
of adequacy, directly in a discrete setting. More generally, this technique can be
used in any computational model that has a compact, fully abstract semantics.
2 Processes, Bisimilarity, and Logics
2.1 Reactive Probabilistic Processes and Strong Bisimilarity
Probabilistic processes can be represented as labeled transitions systems with
probabilistic information used to determine which action is executed or which
state is reached. Following the terminology of [9], we focus on reactive proba-
bilistic processes, where every state has for each action at most one outgoing
distribution over states; the choice among these arbitrarily many, differently la-
beled distributions is nondeterministic. For a countable (i.e., finite or countably
infinite) set X, the set of finitely supported (a.k.a. simple) probability
P distributions
over X is given by D(X) = {∆ : X → R[0,1] | | supp(∆)| < ω, x∈X ∆(x) = 1},
where the support of distribution ∆ is defined as supp(∆) , {x ∈ X | ∆(x) > 0}.
A reactive probabilistic labeled transition system, RPLTS for short, is a triple
(S, A, −→) where S is a countable set of states, A is a countable set of ac-
tions, and −→ ⊆ S × A × D(S) is a transition relation such that, whenever
(s, a, ∆1 ), (s, a, ∆2 ) ∈ −→, then ∆1 = ∆2 .
An RPLTS can be seen as a directed graph whose edges are labeled by
pairs (a, p) ∈ A × R(0,1] . For every s ∈ S and a ∈ A, if there are a-labeled
edges outgoing from s, then these are finitely many (image finiteness), because
the considered distributions are finitely supported, and the numbers on them
a
add up to 1. As usual, we denote (s, a, ∆) ∈ −→ as s −→ ∆, where the set of
Disjunctive Probabilistic Modal Logic 205
reachable states
P coincides with supp(∆). We also define cumulative reachability
as ∆(S 0 ) = s0 ∈S 0 ∆(s0 ) for all S 0 ⊆ S.
Probabilistic bisimilarity for the class of reactive probabilistic processes was
introduced by Larsen and Skou [12]. Let (S, A, −→) be an RPLTS. An equivalence
relation B over S is a probabilistic bisimulation iff, whenever (s1 , s2 ) ∈ B, then for
a a
all actions a ∈ A it holds that, if s1 −→ ∆1 , then s2 −→ ∆2 and ∆1 (C) = ∆2 (C)
for all equivalence classes C ∈ S/B. We say that s1 , s2 ∈ S are probabilistically
bisimilar, written s1 ∼PB s2 , iff there exists a probabilistic bisimulation including
the pair (s1 , s2 ).
2.2 Probabilistic Modal Logics
In our setting, a probabilistic modal logic is a pair formed by a set L of formulas
and an RPLTS-indexed family of satisfaction relations |= ⊆ S × L. The logical
equivalence induced by L over S is defined by letting s1 ∼ =L s2 , where s1 , s2 ∈ S,
iff s1 |= φ ⇐⇒ s2 |= φ for all φ ∈ L. We say that L characterizes a binary
relation R over S when R = ∼ =L .
We are especially interested in probabilistic modal logics characterizing ∼PB .
The logics considered in this paper are similar to Hennessy-Milner logic [10], but
the diamond modality is decorated with a probabilistic lower bound as follows:
PML¬∧ : φ ::= > | ¬φ | φ ∧ φ | haip φ PML∧ : φ ::= > | φ ∧ φ | haip φ
PML¬∨ : φ ::= > | ¬φ | φ ∨ φ | haip φ PML∨ : φ ::= > | φ ∨ φ | haip φ
where p ∈ R[0,1] ; trailing >’s will be omitted for sake of readability. Their seman-
tics with respect to an RPLTS state s is defined as usual, in particular:
a
s |= haip φ ⇐⇒ s −→ ∆ and ∆({s0 ∈ S | s0 |= φ}) ≥ p
Larsen and Skou [12] proved that PML¬∧ (and hence PML¬∨ ) characterizes
∼PB . Desharnais, Edalat, and Panangaden [6] then proved in a measure-theoretic
setting that PML∧ characterizes ∼PB too, and hence negation is not necessary.
This was subsequently redemonstrated by Jacobs and Sokolova [11] in the dual
adjunction framework and by Deng and Wu [5] for a fuzzy extension of RPLTS.
The main aim of this paper is to show that PML∨ suffices as well.
3 Compact Characterization of Probabilistic Bisimilarity
3.1 Coalgebras for Probabilistic Systems
It is well known that the function D defined in Sect. 2.1 extends to a functor
D : Set → Set whose action on morphisms is, for f : X → Y , D(f )(∆) =
λy.∆(f −1 (y)). Then, every RPLTS corresponds to a coalgebra of the functor
BRP : Set → Set, BRP (X) , (D(X) + 1)A . Indeed, for S = (S, A, −→), the corre-
a
sponding coalgebra (S, σ : S → BRP (S)) is σ(s) , λa.(if s −→ ∆ then ∆ else ∗).
A homomorphism h : (S, σ) → (T, τ ) is a function h : S → T that respects the
coalgebraic structures, i.e., τ ◦ h = (BRP h) ◦ σ. We denote by Coalg(BRP ) the
category of BRP -coalgebras and their homomorphisms.
Aczel and Mendler [1] introduced a general notion of bisimulation for coalge-
bras, which in our setting instantiates as follows:
206 M. Bernardo, M. Miculan
Definition 1. Let (S1 , σ1 ), (S2 , σ2 ) be BRP -coalgebras. A relation R ⊆ S1 × S2
is a BRP -bisimulation iff there exists a coalgebra structure ρ : R → BRP R
such that the projections π1 : R → S1 , π2 : R → S2 are homomorphisms (i.e.,
σi ◦ πi = BRP πi ◦ ρ for i = 1, 2). We say that s1 ∈ S1 , s2 ∈ S2 are BRP -bisimilar,
written s1 ∼ s2 , iff there exists a BRP -bisimulation including (s1 , s2 ).
Proposition 1. The probabilistic bisimilarity over an RPLTS (S, A, −→) coin-
cides with the BRP -bisimilarity over the corresponding coalgebra (S, σ).
BRP is finitary (because we restrict to finitely supported distributions) and
hence admits final coalgebra (cf. [3,15] and specifically [14, Thm. 4.6]). The final
coalgebra is unique up-to isomorphism, and can be seen as the RPLTS whose
elements are canonical representatives of all possible behaviors of any RPLTS:
Proposition 2. Let (Z, ζ) be a final BRP -coalgebra. For all z1 , z2 ∈ Z: z1 ∼ z2
iff z1 = z2 .
3.2 Reactive Probabilistic Trees
We now introduce reactive probabilistic trees, a representation of the final BRP -
coalgebra that can be seen as the natural extension to the probabilistic setting
of strongly extensional trees used to represent the final Pf -coalgebra [15].
Definition 2 (RPT ). An (A-labeled) reactive probabilistic tree is a pair (X,
succ) where X ∈ Set and succ : X ×A → Pf (X ×R(0,1] ) are such that the relation
≤ over X, defined by the rules x≤x and x≤y z∈succ(y,a)
x≤z , is a partial order with
a least element, called root, and for all x ∈ X and a ∈ A:
1. the set {y ∈ X | y ≤ x} is finite and well-ordered;
2. for all (x1 , p1 ), (x2 , p2 ) ∈ succ(x, a): if x1 = x2 then p1 = p2 ; if the subtrees
rooted at x1 and x2 are Pisomorphic then x1 = x2 ;
3. if succ(x, a) 6= ∅ then (y,p)∈succ(x,a) p = 1.
Reactive probabilistic trees are unordered trees where each node for each
action has either no successors or a finite set of successors, which are labeled
with positive real numbers that add up to 1; moreover, subtrees rooted at these
successors are all different. See the forthcoming Fig. 1 for some examples. In
particular, the trivial tree is nil , ({⊥}, λx, a.∅).
We denote by RPT, ranged over by t, t1 , t2 , the set of reactive probabilistic
trees (possibly of infinite height), up-to isomorphism. For t = (X, succ), we denote
its root by ⊥t , its a-successors by t(a) , succ(⊥t , a), and the subtree rooted at
x ∈ X by t[x] , ({y ∈ X | x ≤ y}, λy, a.succ(y, a)); thus, ⊥t[x] = x. We define
height : RPT → N ∪ {ω} as height(t) , sup{1 + height(t0 ) | (t0 , p) ∈ t(a), a ∈ A}
with sup ∅ = 0; hence, height(nil) = 0. We denote by RPTf , {t ∈ RPT |
height(t) < ω} the set of reactive probabilistic trees of finite height.
A (possibly infinite) tree can be pruned at any height n, yielding a finite
tree where the removed subtrees are replaced by nil. The “pruning” function
Disjunctive Probabilistic Modal Logic 207
(·)|n : RPT → RPTf , parametric in n, can be defined by first truncating the tree
t at height n, and then collapsing isomorphic subtrees adding their weights.
We have now to show that RPT is (the carrier of) the final BRP -coalgebra
(up-to isomorphism). To this end, we reformulate BRP in a slightly more “rela-
0
P D : Set → Set as follows:
tional” format. We define a functor
0
D X , {∅}∪{U ∈Pf (X×R(0,1] ) | (x,p)∈U p = 1 and (x, p), (x, q) ∈ U ⇒ p = q}
D0 f , λU ∈ D0 X.{(f (x), (x,p)∈U p) | x ∈ π1 (U )}
P
for any f : X → Y.
Proposition 3. D0A = ∼ BRP , and Coalg(D0A ) =∼ Coalg(BRP ); hence the (sup-
0A
ports of the) final D -coalgebra and the final BRP -coalgebra are isomorphic.
RPT is the carrier of the final BRP -coalgebra (up-to isomorphism). In fact,
RPT can be endowed with a D0A -coalgebra structure ρ : RPT → (D0 (RPT))A
defined, for t = (X, succ), as ρ(t)(a) , {(t[x], p) | (x, p) ∈ succ(⊥t , a)}.
Theorem 1. (RPT, ρ) is a final BRP -coalgebra.
By virtue of Thm. 1, given an RPLTS S = (S, A, −→) there exists a unique
coalgebra homomorphism J·K : S → RPT, called the (final) semantics of S, which
associates each state in S with its behavior. This semantics is fully abstract.
Another key property of reactive probabilistic trees is that they are compact: two
different trees can be distinguished by looking at their finite subtrees only.
Theorem 2 (Full abstraction). Let (S, A, −→) be an RPLTS. For all s1 , s2 ∈
S: s1 ∼PB s2 iff Js1 K = Js2 K.
Theorem 3 (Compactness). For all t1 , t2 ∈ RPT: t1 = t2 iff for all n ∈ N :
t1 |n = t2 |n .
Corollary 1. Let (S, A, −→) be an RPLTS. For all s1 , s2 ∈ S: s1 ∼PB s2 iff for
all n ∈ N : Js1 K|n = Js2 K|n .
4 The Discriminating Power of PML∨
By virtue of the categorical construction leading to Cor. 1, in order to prove
that a modal logic characterizes ∼PB over reactive probabilistic processes, it is
enough to show that it can discriminate all reactive probabilistic trees of finite
height. A specific condition on the depth of distinguishing formulas has also to
be satisfied, where depth(φ) is defined as usual:
depth(>) = 0 depth(¬φ0 ) = depth(φ0 ) depth(haip φ0 ) = 1 + depth(φ0 )
depth(φ1 ∧ φ2 ) = depth(φ1 ∨ φ2 ) = max(depth(φ1 ), depth(φ2 ))
Proposition 4. Let L be one of the probabilistic modal logics in Sect. 2.2. If
L characterizes = over RPTf and for any two nodes t1 and t2 of an arbitrary
RPTf model such that t1 6= t2 there exists φ ∈ L distinguishing t1 from t2 such
that depth(φ) ≤ max(height(t1 ), height(t2 )), then L characterizes ∼PB over the
set of RPLTS models.
208 M. Bernardo, M. Miculan
In this section, we show the main result of the paper: the logical equivalence
induced by PML∨ has the same discriminating power as ∼PB . This result is
accomplished in three steps. Firstly, we redemonstrate Larsen and Skou’s result
for PML¬∧ in the RPTf setting, which yields a proof that, with respect to the one
in [12], is simpler and does not require the minimal deviation assumption (i.e., that
the probability associated with any state in the support of the target distribution
of a transition be a multiple of some value). This provides a proof scheme for the
subsequent steps. Secondly, we demonstrate that PML¬∨ characterizes ∼PB by
adapting the proof scheme to cope with the replacement of ∧ with ∨. Thirdly, we
demonstrate that PML∨ characterizes ∼PB by further adapting the proof scheme
to cope with the absence of ¬.
Moreover, we redemonstrate Desharnais, Edalat, and Panangaden’s result for
PML∧ through yet another adaptation of the proof scheme that, unlike the proof
in [6], works directly on discrete state spaces without making use of measure-
theoretic arguments. Avoiding the resort to measure theory was shown to be
possible for the first time by Worrell in an unpublished note cited in [13].
4.1 PML¬∧ Characterizes ∼PB : A New Proof
To show that the logical equivalence induced by PML¬∧ implies node equality
=, we reason on the contrapositive. Given two nodes t1 and t2 such that t1 6= t2 ,
we proceed by induction on the height of t1 to find a distinguishing PML¬∧
formula whose depth is not greater than the heights of t1 and t2 . The idea is to
exploit negation, so to ensure that certain distinguishing formulas are satisfied
by a certain derivative t0 of t1 (rather than the derivatives of t2 different from t0 ),
then take the conjunction of those formulas preceded by a diamond decorated
with the probability for t1 of reaching t0 .
The only non-trivial case is the one in which t1 and t2 enable the same
actions. At least one of those actions, say a, is such that, after performing it,
the two nodes reach two distributions ∆1,a and ∆2,a such that ∆1,a 6= ∆2,a .
Given a node t0 ∈ supp(∆1,a ) such that ∆1,a (t0 ) > ∆2,a (t0 ), by the induction
hypothesis there exists a PML¬∧ formula φ02,j that distinguishes t0 from a specific
t02,j ∈ supp(∆2,a ) \ {t0 }. We can assume that t0 |= φ02,j 6=| t02,j otherwise, thanks
to the presence of negation in PML¬∧ ,Vit would suffice to consider ¬φ02,j .
As a consequence, t1 |= hai∆1,a (t0 ) j φ02,j 6=| t2 because ∆1,a (t0 ) > ∆2,a (t0 )
and ∆2,a (t0 ) is the maximum probabilistic lower bound for which t2 satisfies a
formula of that form. Notice that ∆1,a (t0 ) may not be the maximum V probabilistic
lower bound for which t1 satisfies such a formula, because j φ02,j might be
satisfied by other a-derivatives of t1 in supp(∆1,a ) \ {t0 }.
Theorem 4. Let (T, A, −→) be in RPTf and t1 , t2 ∈ T . Then t1 = t2 iff t1 |=
φ ⇐⇒ t2 |= φ for all φ ∈ PML¬∧ . Moreover, if t1 = 6 t2 , then there exists φ ∈
PML¬∧ distinguishing t1 from t2 such that depth(φ) ≤ max(height(t1 ), height(t2 )).
4.2 PML¬∨ Characterizes ∼PB : Adapting the Proof
Since φ1 ∧ φ2 is logically equivalent to ¬(¬φ1 ∨ ¬φ2 ), it is not surprising that
PML¬∨ characterizes ∼PB too. However, the proof of this result will be useful to
Disjunctive Probabilistic Modal Logic 209
set up an outline of the proof of the main result of this paper, i.e., that PML∨
characterizes ∼PB as well.
Similar to the proof of Thm. 4, also for PML¬∨ we reason on the contrapositive
and proceed by induction. Given t1 and t2 such that t1 6= t2 , we intend to exploit
negation, so to ensure that certain distinguishing formulas are not satisfied by
a certain derivative t0 of t1 (rather than the derivatives of t2 different from t0 ),
then take the disjunction of those formulas preceded by a diamond decorated
with the probability for t2 of not reaching t0 .
In the only non-trivial case, for t0 ∈ supp(∆1,a ) such that ∆1,a (t0 ) > ∆2,a (t0 ),
by the induction hypothesis there exists a PML¬∨ formula φ02,j that distinguishes
t0 from a specific t02,j ∈ supp(∆2,a )\{t0 }. We can assume that t0 6|= φ02,j =| t02,j oth-
erwise, thanks to the presence of negation in PML¬∨ , it would suffice to consider
¬φ02,j . Therefore, t1 6|= hai1−∆2,a (t0 ) j φ02,j =| t2 because 1−∆2,a (t0 ) > 1−∆1,a (t0 )
W
and the maximum probabilistic lower bound for which t1 satisfies a formula of
that form cannot exceed 1 − ∆1,a (t0 ). Notice that 1 − ∆2,a (t0 ) is the maximum
probabilistic lower bound for which t2 satisfies such a formula, because that value
is the probability with which t2 does not reach t0 after performing a.
Theorem 5. Let (T, A, −→) be in RPTf and t1 , t2 ∈ T . Then t1 = t2 iff t1 |=
φ ⇐⇒ t2 |= φ for all φ ∈ PML¬∨ . Moreover, if t1 = 6 t2 , then there exists φ ∈
PML¬∨ distinguishing t1 from t2 such that depth(φ) ≤ max(height(t1 ), height(t2 )).
4.3 Also PML∨ Characterizes ∼PB
The proof that PML∨ characterizes ∼PB is inspired by the one for PML¬∨ , thus
considers the contrapositive and proceeds by induction. In the W only non-trivial
case, we will arrive at a point in which t1 6|= hai1−(∆2,a (t0 )+p) j∈J φ02,j =| t2 for:
– a derivative t0 of t1 , such that ∆1,a (t0 ) > ∆2,a (t0 ), not satisfying any subformula
φ02,j ;
– a suitable probabilistic value p such that ∆2,a (t0 ) + p < 1;
– an index set J identifying certain derivatives of t2 other than t0 .
The choice of t0 is crucial, because negation is no longer available in PML∨ .
Different from the case of PML¬∨ , this induces the introduction of p and the limi-
tation to J in the format of the distinguishing formula. An important observation
is that, in many cases, a disjunctive distinguishing formula can be obtained from
a conjunctive one by suitably increasing some probabilistic lower bounds. An
obvious exception is when the use of conjunction/disjunction is not necessary for
telling two different nodes apart.
Example 1. The nodes t1 and t2 in Fig. 1(a) cannot be distinguished by any
formula in which neither conjunction nor disjunction occurs. It holds that:
t1 |= hai0.5 (hbi1 ∧ hci1 ) 6=| t2 t1 6|= hai1.0 (hbi1 ∨ hci1 ) =| t2
Notice that, when moving from the conjunctive formula to the disjunctive one, the
probabilistic lower bound decorating the a-diamond increases from 0.5 to 1 and
the roles of t1 and t2 with respect to |= are inverted. The situation is similar for
210 M. Bernardo, M. Miculan
(a) t1 t2 (c) t5 t6
a a a a
0.5 0.5 0.5 0.5 0.25 0.25 0.5 0.5
t’1 t’’
1 t’2 t’’
2 t’5 t’’
5’ t’6 t’’
0.5
b c b c b t’’ c b c
(b) t3 t4
a a
0.2 0.2 0.1 0.1 0.1 0.1 0.1 0.1 0.1 0.3 0.2 0.2 0.2
bcd b c b d c d b c d bcd b c b d c d
(d) t7 t8 (e) t9 t10 (f) t11 t12 t13
a a a a a a a
0.5 0.5 0.4 0.4 0.1 0.1 0.7 0.3
t’7 t’8 t’ t’’ t’ t’’’
10’
b b c b c b c t’’ t’’’
10 b c b b
Fig. 1. RPTf models used in the examples of Sects. 4.3 and 4.4.
the nodes t3 and t4 in Fig. 1(b), where two occurrences of conjunction/disjunction
are necessary:
t3 |= hai0.2 (hbi1 ∧ hci1 ∧ hdi1 ) 6=| t4 t3 |= hai0.9 (hbi1 ∨ hci1 ∨ hdi1 ) 6=| t4
but the roles of t3 and t4 with respect to |= cannot be inverted.
Example 2. For the nodes t5 and t6 in Fig. 1(c), it holds that:
t5 6|= hai0.5 (hbi1 ∧ hci1 ) =| t6
If we replace conjunction with disjunction and we vary the probabilistic lower
bound between 0.5 and 1, we produce no disjunctive formula capable of discrim-
inating between t5 and t6 . Nevertheless, a distinguishing formula belonging to
PML∨ exists with no disjunctions at all:
t5 6|= hai0.5 hbi1 =| t6
The examples above show that the increase of some probabilistic lower bounds
when moving from conjunctive distinguishing formulas to disjunctive ones takes
place only in the case that the probabilities of reaching certain nodes have to be
summed up. Additionally, we recall that, in order for two nodes to be related by
∼PB , they must enable the same actions, so focussing on a single action is enough
for discriminating when only disjunction is available. Bearing this in mind, for
any node t of finite height we define the set Φ∨ (t) of PML∨ formulas satisfied by
t featuring:
Disjunctive Probabilistic Modal Logic 211
– probabilistic lower bounds of diamonds that are maximal with respect to
the satisfiability of a formula of that format by t (this is consistent with the
observation in the last sentence before Thm. 5, and keeps the set Φ∨ (t) finite);
– diamonds that arise only from existing transitions that depart from t (so to
avoid useless diamonds in disjunctions and hence keep the set Φ∨ (t) finite);
– disjunctions that stem only from single transitions of different nodes in the
support of a distribution reached W by t (transitions departing from the same
node would result in formulas like h∈H hah iph φh , with ah1 6= ah2 for h1 6= h2 ,
which are useless for discriminating with respect to ∼PB ) and are preceded
by a diamond decorated with the sum of the probabilities assigned to those
nodes by the distribution reached by t.
Definition 3. The set Φ∨ (t) for a node t of finite height is defined by induction
on height(t) as follows:
– If height(t) = 0, then Φ∨ (t) = ∅.
ai
– If height(t) ≥ 1 for t having transitions of the form t −→ ∆i with supp(∆i ) =
{t0i,j | j ∈ Ji } and i ∈ I 6= ∅, then: Φ∨ (t) = {hai i1 | i ∈ I} ∪
.
φ0 | t0 ∈ supp(∆i ), φ0 ∈ Φ∨ (t0 )})
S S W
hplb( {hai i P 0
∆i (ti,j ) i,j,k i,j i,j,k i,j
i∈I ∅6=J 0 ⊆Ji j∈J 0
j∈J 0
where ∨˙ is a variant of ∨ in which identical operands are not admitted (i.e.,
idempotence is forced) and hplb keeps only the formula with the highest prob-
abilistic lower bound decorating the initial ai -diamond among the formulas
differring only for that bound.
To illustrate the definition given above, we exhibit some examples showing
the usefulness of Φ∨ -sets for discrimination purposes. Given two different nodes
that with the same action reach two different distributions, a good criterion for
choosing t0 (a derivative of the first node not satisfying certain formulas, to which
the first distribution assigns a probability greater than the second one) seems to
be the minimality of the Φ∨ -set.
Example 3. For the nodes t7 and t8 in Fig. 1(d), we have:
Φ∨ (t7 ) = {hai1 , hai1 hbi1 } Φ∨ (t8 ) = {hai1 , hai1 hbi1 , hai1 hci1 }
A formula like hai1 (hbi1 ∨ hci1 ) is useless for discriminating between t7 and t8 ,
because disjunction is between two actions enabled by the same node and hence
constituting a nondeterministic choice. Indeed, such a formula is not part of
Φ∨ (t8 ). While in the case of conjunction it is often necessary to concentrate on
several alternative actions, in the case of disjunction it is convenient to focus on
a single action per node when aiming at producing a distinguishing formula.
The fact that hai1 hci1 ∈ Φ∨ (t8 ) is a distinguishing formula can be retrieved
a
as follows. Starting from the two identically labeled transitions t7 −→ ∆7,a and
a
t8 −→ ∆8,a where ∆7,a (t07 ) = 1 = ∆8,a (t08 ) and ∆7,a (t08 ) = 0 = ∆8,a (t07 ), we have:
Φ∨ (t07 ) = {hbi1 } Φ∨ (t08 ) = {hbi1 , hci1 }
If we focus on t7 because ∆7,a (t7 ) > ∆8,a (t07 ) and its Φ∨ -set is minimal, then
0 0
t07 6|= hci1 =| t08 with hci1 ∈ Φ∨ (t08 ) \ Φ∨ (t07 ). As a consequence, t7 6|= hai1 hci1 =| t8
where the value 1 decorating the a-diamond stems from 1 − ∆8,a (t07 ).
212 M. Bernardo, M. Miculan
Example 4. For the nodes t1 and t2 in Fig. 1(a), we have:
Φ∨ (t1 ) = {hai1 , hai0.5 hbi1 , hai0.5 hci1 }
Φ∨ (t2 ) = {hai1 , hai0.5 hbi1 , hai0.5 hci1 , hai1 (hbi1 ∨ hci1 )}
The formulas with two diamonds and no disjunction are identical in the two sets,
so their disjunction hai0.5 hbi1 ∨ hai0.5 hci1 is useless for discriminating between t1
and t2 . Indeed, such a formula is part of neither Φ∨ (t1 ) nor Φ∨ (t2 ). In contrast,
their disjunction in which decorations of identical diamonds are summed up, i.e.,
hai1 (hbi1 ∨ hci1 ), is fundamental. It belongs only to Φ∨ (t2 ) because in the case
of t1 the b-transition and the c-transition depart from the same node, hence no
probabilities can be added.
The fact that hai1 (hbi1 ∨ hci1 ) ∈ Φ∨ (t2 ) is a distinguishing formula can
be retrieved as follows. Starting from the two identically labeled transitions
a a
t1 −→ ∆1,a and t2 −→ ∆2,a where ∆1,a (t01 ) = ∆1,a (t001 ) = 0.5 = ∆2,a (t02 ) =
∆2,a (t2 ) and ∆1,a (t2 ) = ∆1,a (t002 ) = 0 = ∆2,a (t01 ) = ∆2,a (t001 ), we have:
00 0
Φ∨ (t01 ) = {hbi1 , hci1 } Φ∨ (t001 ) = ∅ Φ∨ (t02 ) = {hbi1 } Φ∨ (t002 ) = {hci1 }
If we focus on t001 because ∆1,a (t001 ) > ∆2,a (t001 ) and its Φ∨ -set is minimal, then
t001 6|= hbi1 =| t02 with hbi1 ∈ Φ∨ (t02 ) \ Φ∨ (t001 ) as well as t001 6|= hci1 =| t002 with
hci1 ∈ Φ∨ (t002 )\Φ∨ (t001 ). Thus, t1 6|= hai1 (hbi1 ∨hci1 ) =| t2 where value 1 decorating
the a-diamond stems from 1 − ∆2,a (t001 ).
Example 5. For the nodes t5 and t6 in Fig. 1(c), we have:
Φ∨ (t5 ) = {hai1 , hai0.25 hbi1 , hai0.25 hci1 , hai0.5 (hbi1 ∨ hci1 )}
Φ∨ (t6 ) = {hai1 , hai0.5 hbi1 , hai0.5 hci1 }
The formulas with two diamonds and no disjunction are different in the two sets,
so they are enough for discriminating between t5 and t6 . In contrast, the only
formula with disjunction, occurring in Φ∨ (t5 ), is useless because the probability
decorating its a-diamond is equal to the one decorating the a-diamond of each
of the two formulas with two diamonds in Φ∨ (t6 ).
The fact that hai0.5 hbi1 ∈ Φ∨ (t6 ) is a distinguishing formula can be retrieved
a
as follows. Starting from the two identically labeled transitions t5 −→ ∆5,a and
a
t6 −→ ∆6,a where ∆5,a (t05 ) = ∆5,a (t000 00
5 ) = 0.25, ∆5,a (t ) = 0.5 = ∆6,a (t6 ) =
0
00 0 0 000
∆6,a (t ), and ∆5,a (t6 ) = 0 = ∆6,a (t5 ) = ∆6,a (t5 ), we have:
Φ∨ (t05 ) = {hbi1 } Φ∨ (t000 0
5 ) = {hci1 } Φ∨ (t6 ) = {hbi1 , hci1 } Φ∨ (t ) = ∅
00
00
Notice that t might be useless for discriminating purposes because it has the
same probability in both distributions, so we exclude it. If we focus on t000 5 because
∆5,a (t000
5 ) > ∆ (t
6,a 5
000
) and its Φ∨ -set is minimal after the exclusion of t00 , then
000 0 0 000
t5 6|= hbi1 =| t6 with hbi1 ∈ Φ∨ (t6 ) \ Φ∨ (t5 ), while no distinguishing formula is
considered with respect to t00 as element of supp(∆6,a ) due to the exclusion of
t00 itself. As a consequence, t5 6|= hai0.5 hbi1 =| t6 where the value 0.5 decorating
the a-diamond stems from 1 − (∆6,a (t000 00
5 ) + p) with p = ∆6,a (t ). The reason for
subtracting the probability that t6 reaches t after performing a is that t00 6|= hbi1 .
00
We conclude by observing that focussing on t00 as derivative with the min-
imum Φ∨ -set is indeed problematic, because it would result in hai0.5 hbi1 when
considering t00 as derivative of t5 , but it would result in hai0.5 (hbi1 ∨ hci1 ) when
considering t00 as derivative of t6 , with the latter formula not distinguishing be-
Disjunctive Probabilistic Modal Logic 213
tween t5 and t6 . Moreover, when focussing on t000 0
5 , no formula φ could have been
000 0 00 00 000
found such that t5 6|= φ =| t as Φ∨ (t ) ( Φ∨ (t5 ).
The last example shows that, in the general format hai1−(∆2,a (t0 )+p) j∈J φ02,j
W
for the PML∨ distinguishing formula mentioned at the beginning of this subsec-
tion, the set J only contains any derivative of the second node different from t0
to which the two distributions assign two different probabilities. No derivative
of the two original nodes having the same probability in both distributions is
taken into account even if its Φ∨ -set is minimal – because it might be useless for
discriminating purposes – nor is it included in J – because there might be no
formula satisfied by this node when viewed as a derivative of the second node,
which is not satisfied by t0 . Furthermore, the value p is the probability that the
second node reaches the excluded derivatives that do not satisfy j∈J φ02,j ; note
W
that the first node reaches those derivatives with the same probability p.
We present two additional examples illustrating some technicalities of Def. 3.
The former example shows the usefulness of the operator ∨˙ and of the function
hplb for selecting the right t0 on the basis of the minimality of its Φ∨ -set among the
derivatives of the first node to which the first distribution assigns a probability
greater than the second one. The latter example emphasizes the role played, for
the same purpose as before, by formulas occurring in a Φ∨ -set whose number of
nested diamonds is not maximal.
Example 6. For the nodes t9 and t10 in Fig. 1(e), we have:
Φ∨ (t9 ) = {hai1 , hai0.5 hbi1 , hai0.5 hci1 }
Φ∨ (t10 ) = {hai1 , hai0.5 hbi1 , hai0.5 hci1 , hai0.6 (hbi1 ∨ hci1 )}
a a
Starting from the two identically labeled transitions t9 −→ ∆9,a and t10 −→ ∆10,a
where ∆9,a (t0 ) = ∆9,a (t00 ) = 0.5, ∆10,a (t0 ) = ∆10,a (t00 ) = 0.4, ∆10,a (t000 10 ) =
∆10,a (t0000 000 0000
10 ) = 0.1, and ∆9,a (t10 ) = ∆9,a (t10 ) = 0, we have:
Φ∨ (t0 ) = {hbi1 , hci1 } Φ∨ (t00 ) = ∅ Φ∨ (t000 0000
10 ) = {hbi1 } Φ∨ (t10 ) = {hci1 }
00 00 00
If we focus on t because ∆9,a (t ) > ∆10,a (t ) and its Φ∨ -set is minimal, then
t00 6|= hbi1 =| t0 with hbi1 ∈ Φ∨ (t0 ) \ Φ∨ (t00 ), t00 6|= hbi1 =| t000 000
10 with hbi1 ∈ Φ∨ (t10 ) \
00 00 0000 0000 00
Φ∨ (t ), and t 6|= hci1 =| t10 with hci1 ∈ Φ∨ (t10 )\Φ∨ (t ). Thus, t9 6|= hai0.6 (hbi1 ∨
hci1 ) =| t10 where the formula belongs to Φ∨ (t10 ) and the value 0.6 decorating
the a-diamond stems from 1 − ∆10,a (t00 ).
If ∨ were used in place of ∨, ˙ then in Φ∨ (t10 ) we would also have formulas
like hai0.5 (hbi1 ∨ hbi1 ) and hai0.5 (hci1 ∨ hci1 ). These are useless in that logically
equivalent to other formulas already in Φ∨ (t10 ) in which disjunction does not
occur and, most importantly, would apparently augment the size of Φ∨ (t10 ), an
inappropriate fact in the case that t10 were a derivative of some other node
instead of being the root of a tree.
If hplb were not used, then in Φ∨ (t10 ) we would also have formulas like
hai0.1 hbi1 , hai0.4 hbi1 , hai0.1 hci1 , and hai0.4 hci1 , in which the probabilistic lower
bounds of the a-diamonds are not maximal with respect to the satisfiability of
formulas of that form by t10 ; those with maximal probabilistic lower bounds
associated with a-diamonds are hai0.5 hbi1 and hai0.5 hci1 , which already belong
to Φ∨ (t10 ). In the case that t9 and t10 were derivatives of two nodes under
214 M. Bernardo, M. Miculan
comparison instead of being the roots of two trees, the presence of those additional
formulas in Φ∨ (t10 ) may lead to focus on t10 instead of t9 – for reasons that will
be clear in Ex. 8 – thereby producing no distinguishing formula.
Example 7. For the nodes t11 , t12 , t13 in Fig. 1(f), we have:
Φ∨ (t11 ) = {hai1 } Φ∨ (t12 ) = {hai1 , hai1 hbi1 } Φ∨ (t13 ) = {hai1 , hai0.7 hbi1 }
Let us view them as derivatives of other nodes, rather than roots of trees. The
presence of formula hai1 in Φ∨ (t12 ) and Φ∨ (t13 ) – although it has not the maxi-
mum number of nested diamonds in those two sets – ensures the minimality of
Φ∨ (t11 ) and hence that t11 is selected for building a distinguishing formula. If
hai1 were not in Φ∨ (t12 ) and Φ∨ (t13 ), then t12 and t13 could be selected, but no
distinguishing formula satisfied by t11 could be obtained.
The criterion for selecting the right t0 based on the minimality of its Φ∨ -set
has to take into account a further aspect related to formulas without disjunctions.
If two derivatives – with different probabilities in the two distributions – have
the same formulas without disjunctions in their Φ∨ -sets, then a distinguishing
formula for the two nodes will have disjunctions in it (see Exs. 4 and 6). If the
formulas without disjunctions are different between the two Φ∨ -sets, then one of
them will tell the two derivatives apart (see Ex. 3).
A particular instance of the second case is the one in which for each formula
without disjunctions in one of the two Φ∨ -sets there is a variant in the other
Φ∨ -set – i.e., a formula without disjunctions that has the same format but may
differ for the values of some probabilistic lower bounds – and vice versa. In
this event, regardless of the minimality of the Φ∨ -sets, it has to be selected the
derivative such that (i) for each formula without disjunctions in its Φ∨ -set there
exists a variant in the Φ∨ -set of the other derivative such that the probabilistic
lower bounds in the former formula are ≤ than the corresponding bounds in the
latter formula and (ii) at least one probabilistic lower bound in a formula without
disjunctions in the Φ∨ -set of the selected derivative is < than the corresponding
bound in the corresponding variant in the Φ∨ -set of the other derivative. We say
that the Φ∨ -set of the selected derivative is a (≤, <)-variant of the Φ∨ -set of the
other derivative.
Example 8. Let us view the nodes t5 and t6 in Fig. 1(c) as derivatives of other
nodes, rather than roots of trees. Based on their Φ∨ -sets shown in Ex. 5, we
should focus on t6 because Φ∨ (t6 ) contains fewer formulas. However, by so doing,
we would be unable to find a distinguishing formula in Φ∨ (t5 ) that is not satisfied
by t6 . Indeed, if we look carefully at the formulas without disjunctions in Φ∨ (t5 )
and Φ∨ (t6 ), we note that they differ only for their probabilistic lower bounds:
hai1 ∈ Φ∨ (t6 ) is a variant of hai1 ∈ Φ∨ (t5 ), hai0.5 hbi1 ∈ Φ∨ (t6 ) is a variant of
hai0.25 hbi1 ∈ Φ∨ (t5 ), and hai0.5 hci1 ∈ Φ∨ (t6 ) is a variant of hai0.25 hci1 ∈ Φ∨ (t5 ).
Therefore, we must focus on t5 because Φ∨ (t5 ) contains formulas without dis-
junctions such as hai0.25 hbi1 and hai0.25 hci1 having smaller bounds: Φ∨ (t5 ) is a
(≤, <)-variant of Φ∨ (t6 ).
Consider now the nodes t9 and t10 in Fig. 1(e), whose Φ∨ -sets are shown in
Ex. 6. If function hplb were not used and hence Φ∨ (t10 ) also contained hai0.1 hbi1 ,
Disjunctive Probabilistic Modal Logic 215
hai0.4 hbi1 , hai0.1 hci1 , and hai0.4 hci1 , then the formulas without disjunctions in
Φ∨ (t9 ) would no longer be equal to those in Φ∨ (t10 ). More precisely, the formulas
without disjunctions would be similar between the two sets, with those in Φ∨ (t10 )
having smaller probabilistic lower bounds, so that we would erroneously focus
on t10 .
Summing up, in the PML∨ distinguishing formula hai1−(∆2,a (t0 )+p) j∈J φ02,j ,
W
the steps for choosing the derivative t0 , on the basis of which each subformula
φ02,j is then generated so that it is not satisfied by t0 itself, are the following:
1. Consider only derivatives to which ∆1,a assigns a probability greater than
the one assigned by ∆2,a .
2. Within the previous set, eliminate all the derivatives whose Φ∨ -sets have
(≤, <)-variants.
3. Among the remaining derivatives, focus on one of those having a minimal
Φ∨ -set.
Theorem 6. Let (T, A, −→) be in RPTf and t1 , t2 ∈ T . Then t1 = t2 iff t1 |=
φ ⇐⇒ t2 |= φ for all φ ∈ PML∨ . Moreover, if t1 6= t2 , then there exists φ ∈
PML∨ distinguishing t1 from t2 such that depth(φ) ≤ max(height(t1 ), height(t2 )).
4.4 PML∧ Characterizes ∼PB : A Direct Proof for Discrete Systems
By adapting the proof of Thm. 6 consistently with the proof of Thm. 4, we can
also prove that PML∧ characterizes ∼PB by working directly on discrete state
spaces.
The idea is to obtain t1 |= hai∆1,a (t0 )+p j∈J φ02,j 6=| t2 . For any node t of
V
finite height, we define the set Φ∧ (t) of PML∧ formulas satisfied by t featuring,
in addition to maximal probabilistic lower bounds and diamonds arising only
from transitions of t as for Φ∨ (t), conjunctions that (i) stem only from transi-
tions departing from the same node in the support of a distribution reached by t
and (ii) are preceded by a diamond decorated with the sum of the probabilities
assigned by that distribution to that node and other nodes with the same tran-
ai
sitions considered for that node. Given t having transitions of the form t −→ ∆i
with supp(∆i ) = {t0i,j | j ∈ Ji } and i ∈ I 6= ∅, we let: Φ∧ (t) = {hai i1 | i ∈ I} ∪
V 0
6 K 0 ⊆ Ki,j , t0i,j ∈ supp(∆i ), φ0i,j,k ∈ Φ∧ (t0i,j ) |})
S
splb({| hai i∆i (t0i,j ) φi,j,k | ∅ =
i∈I k∈K 0
where {| and |} are multiset parentheses, Ki,j is the index set for Φ∧ (t0i,j ), and
function splb merges all formulas possibly differring only for the probabilistic
lower bound decorating their initial ai -diamond by summing up those bounds
(such formulas stem from different nodes in supp(∆i )).
A good criterion for choosing t0 occurring in the PML∧ distinguishing formula
at the beginning of this subsection is the maximality of the Φ∧ -set. Moreover,
in that formula J only contains any derivative of the second node different
from t0 to which the two distributions assign two different probabilities, while
p is the probability of reaching derivatives having the same probability in both
distributions that satisfy j∈J φ02,j . Finally, when selecting t0 , we have to leave
V
out all the derivatives whose Φ∧ -sets have (≤, <)-variants.
216 M. Bernardo, M. Miculan
Theorem 7. Let (T, A, −→) be in RPTf and t1 , t2 ∈ T . Then t1 = t2 iff t1 |=
φ ⇐⇒ t2 |= φ for all φ ∈ PML∧ . Moreover, if t1 6= t2 , then there exists φ ∈
PML∧ distinguishing t1 from t2 such that depth(φ) ≤ max(height(t1 ), height(t2 )).
5 Conclusions
In this paper, we have studied modal logic characterizations of strong bisimilarity
over reactive probabilistic processes. Starting from previous work by Larsen and
Skou [12] (who provided a characterization based on a probabilistic extension
of Hennessy-Milner logic) and by Desharnais, Edalat, and Panangaden [6] (who
showed that negation is not necessary), we have proved that conjunction can
be replaced by disjunction without having to reintroduce negation. Thus, in the
reactive probabilistic setting, conjunction and disjunction are interchangeable to
characterize (bi)simulation equivalence, while they are both necessary for simu-
lation preorder [7]. As a side result, with our proof technique we have provided
alternative proofs of the expressiveness of PML¬∧ and PML∧ .
The intuition behind our result is that from a conjunctive distinguishing
formula it is often possible to derive a disjunctive one by suitably increasing some
probabilistic lower bounds. On the model side, this corresponds to summing up
the probabilities of reaching certain states that are in the support of a target
distribution. In fact, a state of an RPLTS can be given a semantics as a reactive
probabilistic tree, and hence it is characterized by the countable set of formulas
(approximated by the Φ∨ -set) obtained by doing finite visits of the tree.
On the application side, the PML∨ -based characterization of bisimilarity
over reactive probabilistic processes may help to prove a conjecture in [4]. This
work studies the discriminating power of three different testing equivalences
respectively using reactive probabilistic tests, fully nondeterministic tests, and
nondeterministic and probabilistic tests. Numerous examples lead to conjecture
that testing equivalence based on nondeterministic and probabilistic tests may
have the same discriminating power as bisimilarity. Given two ∼PB -inequivalent
reactive probabilistic processes, the idea of the tentative proof is to build a dis-
tinguishing nondeterministic and probabilistic test from a distinguishing PML∧
formula. One of the main difficulties with carrying out such a proof, i.e., the fact
that choices within tests fit well together with disjunction rather than conjunction,
may be overcome by starting from a distinguishing PML∨ formula.
References
1. P. Aczel and N. Mendler. A final coalgebra theorem. In Proc. of the 3rd Conf. on
Category Theory and Computer Science (CTCS 1989), volume 389 of LNCS, pages
357–365. Springer, 1989.
2. C. Baier and M. Kwiatkowska. Domain equations for probabilistic processes. Math-
ematical Structures in Computer Science, 10:665–717, 2000.
3. M. Barr. Terminal coalgebras in well-founded set theory. Theoretical Computer
Science, 114:299–315, 1993.
Disjunctive Probabilistic Modal Logic 217
4. M. Bernardo, D. Sangiorgi, and V. Vignudelli. On the discriminating power of test-
ing equivalences for reactive probabilistic systems: Results and open problems. In
Proc. of the 11th Int. Conf. on the Quantitative Evaluation of Systems (QEST 2014),
volume 8657 of LNCS, pages 281–296. Springer, 2014.
5. Y. Deng and H. Wu. Modal characterisations of probabilistic and fuzzy bisim-
ulations. In Proc. of the 16th Int. Conf. on Formal Engineering Methods
(ICFEM 2014), volume 8829 of LNCS, pages 123–138. Springer, 2014.
6. J. Desharnais, A. Edalat, and P. Panangaden. Bisimulation for labelled Markov
processes. Information and Computation, 179:163–193, 2002.
7. J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. Approximating
labelled Markov processes. Information and Computation, 184:160–200, 2003.
8. R.J. van Glabbeek. The linear time – branching time spectrum I. In Handbook of
Process Algebra, pages 3–99. Elsevier, 2001.
9. R.J. van Glabbeek, S.A. Smolka, and B. Steffen. Reactive, generative and stratified
models of probabilistic processes. Information and Computation, 121:59–80, 1995.
10. M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency.
Journal of the ACM, 32:137–162, 1985.
11. B. Jacobs and A. Sokolova. Exemplaric expressivity of modal logics. Journal of
Logic and Computation, 20:1041–1068, 2010.
12. K.G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information
and Computation, 94:1–28, 1991.
13. P. Panangaden. Probabilistic bisimulation. In Advanced Topics in Bisimulation
and Coinduction, pages 300–334. Cambridge University Press, 2011.
14. E.P. de Vink and J.J.M.M. Rutten. Bisimulation for probabilistic transition systems:
A coalgebraic approach. Theoretical Computer Science, 221:271–293, 1999.
15. J. Worrell. On the final sequence of a finitary set functor. Theoretical Computer
Science, 338:184–199, 2005.