Introduction

Since its introduction [12], probabilistic bisimilarity has been used to compare probabilistic systems. It corresponds to Milner's strong bisimilarity for nondeterministic 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 a p φ, 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]).

In this paper, we show that ∨ can be used in place of ∧ without having to reintroduce negation: the constructs , ∨, and a p suffice to characterize bisimilarity on reactive probabilistic systems. The intuition is that from a conjunctive distinguishing formula we can often derive a disjunctive one by suitably increasing 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 semantics 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.

Processes, Bisimilarity, and Logics

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 probabilistic processes, where every state has for each action at most one outgoing distribution over states; the choice among these arbitrarily many, differently labeled distributions is nondeterministic. For a countable (i.e., finite or countably infinite) set X, the set of finitely supported (a.k.a. simple) probability 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 actions, 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 add up to 1. As usual, we denote (s, a, ∆) ∈ −→ as s a −→ ∆, where the set of reachable states coincides with supp(∆). We also define cumulative reachability as ∆(S ) = s ∈S ∆(s ) for all S ⊆ 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 (s 1 , s 2 ) ∈ B, then for all actions a ∈ A it holds that, if

s 1 a −→ ∆ 1 , then s 2 a −→ ∆ 2 and ∆ 1 (C) = ∆ 2 (C)

for all equivalence classes C ∈ S/B. We say that s 1 , s 2 ∈ S are probabilistically bisimilar, written s 1 ∼ PB s 2 , iff there exists a probabilistic bisimulation including the pair (s 1 , s 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 s 1 ∼ =L s 2 , where s 1 , s 2 ∈ S, iff s 1 |= φ ⇐⇒ s 2 |= φ 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 ¬∧ :

φ ::= | ¬φ | φ ∧ φ | a p φ PML ∧ : φ ::= | φ ∧ φ | a p φ PML ¬∨ : φ ::= | ¬φ | φ ∨ φ | a p φ PML ∨ : φ ::= | φ ∨ φ | a p φ where p ∈ R [0,1

] ; trailing 's will be omitted for sake of readability. Their semantics with respect to an RPLTS state s is defined as usual, in particular:

s |= a p φ ⇐⇒ s a −→ ∆ and ∆({s ∈ S | s |= φ})

≥ 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.

Compact Characterization of Probabilistic Bisimilarity

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 B RP : Set → Set, B RP (X) (D(X) + 1) A . Indeed, for S = (S, A, −→), the corresponding coalgebra (S, σ :

S → B RP (S)) is σ(s) λa.(if s a −→ ∆ then ∆ else * ). A homomorphism h : (S, σ) → (T, τ ) is a function h : S → T that respects the coalgebraic structures, i.e., τ • h = (B RP h) • σ.

We denote by Coalg(B RP ) the category of B RP -coalgebras and their homomorphisms.

Aczel and Mendler [1] introduced a general notion of bisimulation for coalgebras, which in our setting instantiates as follows:

Definition 1. Let (S 1 , σ 1 ), (S 2 , σ 2 ) be B RP -coalgebras. A relation R ⊆ S 1 × S 2

is a B RP -bisimulation iff there exists a coalgebra structure ρ : R → B RP R such that the projections π 1 : R → S 1 , π 2 : R → S 2 are homomorphisms (i.e., σ i • π i = B RP π i • ρ for i = 1, 2). We say that s 1 ∈ S 1 , s 2 ∈ S 2 are B RP -bisimilar, written s 1 ∼ s 2 , iff there exists a B RP -bisimulation including (s 1 , s 2 ). Proposition 1. The probabilistic bisimilarity over an RPLTS (S, A, −→) coincides with the B RP -bisimilarity over the corresponding coalgebra (S, σ). B RP 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 B RP -coalgebra. For all z 1 , z 2 ∈ Z: z 1 ∼ z 2 iff z 1 = z 2 .

Reactive Probabilistic Trees

We now introduce reactive probabilistic trees, a representation of the final B RPcoalgebra that can be seen as the natural extension to the probabilistic setting of strongly extensional trees used to represent the final P f -coalgebra [15].

Definition 2 (RPT ).

An (A-labeled) reactive probabilistic tree is a pair (X, succ) where X ∈ Set and succ : X ×A → P f (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 (x 1 , p 1 ), (x 2 , p 2 ) ∈ succ(x, a): if x 1 = x 2 then p 1 = p 2 ; if the subtrees rooted at x 1 and x 2 are isomorphic then x 1 = x 2 ; 3. if succ(x, a) = ∅ 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, t 1 , t 2 , 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(t ) | (t , p) ∈ t(a), a ∈ A} with sup ∅ = 0; hence, height(nil) = 0. We denote by RPT f {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 (•)| n : RPT → RPT f , 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 B RP -coalgebra (up-to isomorphism). To this end, we reformulate B RP in a slightly more "relational" format. We define a functor D : Set → Set as follows: RPT is the carrier of the final B RP -coalgebra (up-to isomorphism). In fact, RPT can be endowed with a D A -coalgebra structure ρ : RPT → (D (RPT)) A defined, for t = (X, succ), as ρ(t)(a)

D X {∅}∪{U ∈P f (X×R (0,1] ) | (x,p)∈U p = 1 and (x, p), (x, q) ∈ U ⇒ p = q} D f λU ∈ D X.{(f (x), (x,p)∈U p) | x ∈ π 1 (U )} for any f : X → Y.{(t[x], p) | (x, p) ∈ succ(⊥ t , a)}. Theorem 1. (RPT, ρ) is a final B RP -coalgebra.

By virtue of Thm. 1, given an RPLTS S = (S, A, −→) there exists a unique coalgebra homomorphism • : 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 alls 1 , s 2 ∈ S: s 1 ∼ PB s 2 iff s 1 = s 2 . Theorem 3 (Compactness). For all t 1 , t 2 ∈ RPT: t 1 = t 2 iff for all n ∈ N : t 1 | n = t 2 | n . Corollary 1. Let (S, A, −→) be an RPLTS. For all s 1 , s 2 ∈ S: s 1 ∼ PB s 2 iff for all n ∈ N : s 1 | n = s 2 | n .

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(¬φ ) = depth(φ ) depth( a p φ ) = 1 + depth(φ ) 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 RPT f and for any two nodes t 1 and t 2 of an arbitrary RPT f model such that t 1 = t 2 there exists φ ∈ L distinguishing t 1 from t 2 such that depth(φ) ≤ max(height(t 1 ), height(t 2 )), then L characterizes ∼ PB over the set of RPLTS models.

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 RPT f 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 measuretheoretic 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].

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 t 1 and t 2 such that t 1 = t 2 , we proceed by induction on the height of t 1 to find a distinguishing PML ¬∧ formula whose depth is not greater than the heights of t 1 and t 2 . The idea is to exploit negation, so to ensure that certain distinguishing formulas are satisfied by a certain derivative t of t 1 (rather than the derivatives of t 2 different from t ), then take the conjunction of those formulas preceded by a diamond decorated with the probability for t 1 of reaching t .

The only non-trivial case is the one in which t 1 and t 2 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 = ∆ 2,a . Given a node t ∈ supp(∆ 1,a ) such that ∆ 1,a (t ) > ∆ 2,a (t ), by the induction hypothesis there exists a PML ¬∧ formula φ 2,j that distinguishes t from a specific t 2,j ∈ supp(∆ 2,a ) \ {t }. We can assume that t |= φ 2,j =| t 2,j otherwise, thanks to the presence of negation in PML ¬∧ , it would suffice to consider ¬φ 2,j .

As a consequence, t 1 |= a ∆1,a(t ) j φ 2,j =| t 2 because ∆ 1,a (t ) > ∆ 2,a (t ) and ∆ 2,a (t ) is the maximum probabilistic lower bound for which t 2 satisfies a formula of that form. Notice that ∆ 1,a (t ) may not be the maximum probabilistic lower bound for which t 1 satisfies such a formula, because j φ 2,j might be satisfied by other a-derivatives of t 1 in supp(∆ 1,a ) \ {t }.

Theorem 4. Let (T, A, −→) be in RPT f and t 1 , t 2 ∈ T . Then t 1 = t 2 iff t 1 |= φ ⇐⇒ t 2 |= φ for all φ ∈ PML ¬∧ . Moreover, if t 1 = t 2 , then there exists φ ∈ PML ¬∧ distinguishing t 1 from t 2 such that depth(φ) ≤ max(height(t 1 ), height(t 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 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 t 1 and t 2 such that t 1 = t 2 , we intend to exploit negation, so to ensure that certain distinguishing formulas are not satisfied by a certain derivative t of t 1 (rather than the derivatives of t 2 different from t ), then take the disjunction of those formulas preceded by a diamond decorated with the probability for t 2 of not reaching t .

In the only non-trivial case, for t ∈ supp(∆ 1,a ) such that ∆ 1,a (t ) > ∆ 2,a (t ), by the induction hypothesis there exists a PML ¬∨ formula φ 2,j that distinguishes t from a specific t 2,j ∈ supp(∆ 2,a )\{t }. We can assume that t |= φ 2,j =| t 2,j otherwise, thanks to the presence of negation in PML ¬∨ , it would suffice to consider ¬φ 2,j . Therefore,

t 1 |= a 1−∆2,a(t ) j φ 2,j =| t 2 because 1−∆ 2,a (t ) > 1−∆ 1,a (t )

and the maximum probabilistic lower bound for which t 1 satisfies a formula of that form cannot exceed 1 − ∆ 1,a (t ). Notice that 1 − ∆ 2,a (t ) is the maximum probabilistic lower bound for which t 2 satisfies such a formula, because that value is the probability with which t 2 does not reach t after performing a.

Theorem 5. Let (T, A, −→) be in RPT f and t 1 , t 2 ∈ T . Then t 1 = t 2 iff t 1 |= φ ⇐⇒ t 2 |= φ for all φ ∈ PML ¬∨ . Moreover, if t 1 = t 2 , then there exists φ ∈ PML ¬∨ distinguishing t 1 from t 2 such that depth(φ) ≤ max(height(t 1 ), height(t 2 )).

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 only non-trivial case, we will arrive at a point in which t 1 |= a 1−(∆2,a(t )+p) j∈J φ 2,j =| t 2 for:

a derivative t of t 1 , such that ∆ 1,a (t ) > ∆ 2,a (t ), not satisfying any subformula φ 2,j ; a suitable probabilistic value p such that ∆ 2,a (t ) + p < 1; an index set J identifying certain derivatives of t 2 other than t .

The choice of t is crucial, because negation is no longer available in PML ∨ . Different from the case of PML ¬∨ , this induces the introduction of p and the limitation 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 t 1 and t 2 in Fig. 1(a) cannot be distinguished by any formula in which neither conjunction nor disjunction occurs. It holds that:

t 1 |= a 0.5 ( b 1 ∧ c 1 ) =| t 2 t 1 |= a 1.0 ( b 1 ∨ c 1 ) =| t 2

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 t 1 and t 2 with respect to |= are inverted. The situation is similar for the nodes t 3 and t 4 in Fig. 1(b), where two occurrences of conjunction/disjunction are necessary:

t 3 |= a 0.2 ( b 1 ∧ c 1 ∧ d 1 ) =| t 4 t 3 |= a 0.9 ( b 1 ∨ c 1 ∨ d 1 )

=| t 4 but the roles of t 3 and t 4 with respect to |= cannot be inverted.

Example 2. For the nodes t 5 and t 6 in Fig. 1(c), it holds that: t 5 |= a 0.5 ( b 1 ∧ c 1 ) =| t 6 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 discriminating between t 5 and t 6 . Nevertheless, a distinguishing formula belonging to PML ∨ exists with no disjunctions at all:

t 5 |= a 0.5 b 1 =| t 6

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:

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 by t (transitions departing from the same node would result in formulas like h∈H a h p h φ h , with a h1 = a h2 for h 1 = h 2 , 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) = ∅. -If height(t) ≥ 1 for t having transitions of the form t ai −→ ∆ i with supp(∆ i ) = {t i,j | j ∈ J i } and i ∈ I = ∅, then: Φ ∨ (t) = { a i 1 | i ∈ I} ∪ i∈I hplb( ∅ =J ⊆Ji { a i j∈J ∆i(t i,j ) . j∈J φ i,j,k | t i,j ∈ supp(∆ i ), φ i,j,k ∈ Φ ∨ (t i,j )})

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 probabilistic lower bound decorating the initial a i -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 t (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 t 7 and t 8 in Fig. 1(d), we have:

Φ ∨ (t 7 ) = { a 1 , a 1 b 1 } Φ ∨ (t 8 ) = { a 1 , a 1 b 1 , a 1 c 1 } A formula like a 1 ( b 1 ∨ c 1 )

is useless for discriminating between t 7 and t 8 , 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 Φ ∨ (t 8 ). 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 a 1 c 1 ∈ Φ ∨ (t 8 ) is a distinguishing formula can be retrieved as follows. Starting from the two identically labeled transitions t 7 a −→ ∆ 7,a and t 8 a −→ ∆ 8,a where ∆ 7,a (t 7 ) = 1 = ∆ 8,a (t 8 ) and ∆ 7,a (t 8 ) = 0 = ∆ 8,a (t 7 ), we have:

Φ ∨ (t 7 ) = { b 1 } Φ ∨ (t 8 ) = { b 1 , c 1 } If we focus on t 7 because ∆ 7,a (t 7 ) > ∆ 8,a (t 7 ) and its Φ ∨ -set is minimal, then t 7 |= c 1 =| t 8 with c 1 ∈ Φ ∨ (t 8 ) \ Φ ∨ (t 7 ). As a consequence, t 7 |= a 1 c 1 =| t 8

where the value 1 decorating the a-diamond stems from 1 − ∆ 8,a (t 7 ).

Example 4. For the nodes t 1 and t 2 in Fig. 1(a), we have:

Φ ∨ (t 1 ) = { a 1 , a 0.5 b 1 , a 0.5 c 1 } Φ ∨ (t 2 ) = { a 1 , a 0.5 b 1 , a 0.5 c 1 , a 1 ( b 1 ∨ c 1 )

} The formulas with two diamonds and no disjunction are identical in the two sets, so their disjunction a 0.5 b 1 ∨ a 0.5 c 1 is useless for discriminating between t 1 and t 2 . Indeed, such a formula is part of neither Φ ∨ (t 1 ) nor Φ ∨ (t 2 ). In contrast, their disjunction in which decorations of identical diamonds are summed up, i.e., a 1 ( b 1 ∨ c 1 ), is fundamental. It belongs only to Φ ∨ (t 2 ) because in the case of t 1 the b-transition and the c-transition depart from the same node, hence no probabilities can be added.

The fact that a

1 ( b 1 ∨ c 1 ) ∈ Φ ∨ (t 2

) is a distinguishing formula can be retrieved as follows. Starting from the two identically labeled transitions

t 1 a −→ ∆ 1,a and t 2 a −→ ∆ 2,a where ∆ 1,a (t 1 ) = ∆ 1,a (t 1 ) = 0.5 = ∆ 2,a (t 2 ) = ∆ 2,a (t 2 ) and ∆ 1,a (t 2 ) = ∆ 1,a (t 2 ) = 0 = ∆ 2,a (t 1 ) = ∆ 2,a (t 1 ), we have: Φ ∨ (t 1 ) = { b 1 , c 1 } Φ ∨ (t 1 ) = ∅ Φ ∨ (t 2 ) = { b 1 } Φ ∨ (t 2 ) = { c 1 } If we focus on t 1 because ∆ 1,a (t 1 ) > ∆ 2,a (t 1 ) and its Φ ∨ -set is minimal, then t 1 |= b 1 =| t 2 with b 1 ∈ Φ ∨ (t 2 ) \ Φ ∨ (t 1 ) as well as t 1 |= c 1 =| t 2 with c 1 ∈ Φ ∨ (t 2 )\Φ ∨ (t 1 ). Thus, t 1 |= a 1 ( b 1 ∨ c 1 ) =| t 2

where value 1 decorating the a-diamond stems from 1 − ∆ 2,a (t 1 ).

Example 5. For the nodes t 5 and t 6 in Fig. 1(c), we have:

Φ ∨ (t 5 ) = { a 1 , a 0.25 b 1 , a 0.25 c 1 , a 0.5 ( b 1 ∨ c 1 )} Φ ∨ (t 6 ) = { a 1 , a 0.5 b 1 , a 0.5 c 1 }

The formulas with two diamonds and no disjunction are different in the two sets, so they are enough for discriminating between t 5 and t 6 . In contrast, the only formula with disjunction, occurring in Φ ∨ (t 5 ), 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 Φ ∨ (t 6 ).

The fact that a 0.5 b 1 ∈ Φ ∨ (t 6 ) is a distinguishing formula can be retrieved as follows. Starting from the two identically labeled transitions t 5 a −→ ∆ 5,a and t 6 a −→ ∆ 6,a where ∆ 5,a (t 5 ) = ∆ 5,a (t 5 ) = 0.25, ∆ 5,a (t ) = 0.5 = ∆ 6,a (t 6 ) = ∆ 6,a (t ), and ∆ 5,a (t 6 ) = 0 = ∆ 6,a (t 5 ) = ∆ 6,a (t 5 ), we have:

Φ ∨ (t 5 ) = { b 1 } Φ ∨ (t 5 ) = { c 1 } Φ ∨ (t 6 ) = { b 1 , c 1 } Φ ∨ (t )

= ∅ 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 t 5 because ∆ 5,a (t 5 ) > ∆ 6,a (t 5 ) and its Φ ∨ -set is minimal after the exclusion of t , then

t 5 |= b 1 =| t 6 with b 1 ∈ Φ ∨ (t 6 ) \ Φ ∨ (t 5

), while no distinguishing formula is considered with respect to t as element of supp(∆ 6,a ) due to the exclusion of t itself. As a consequence, t 5 |= a 0.5 b 1 =| t 6 where the value 0.5 decorating the a-diamond stems from 1 − (∆ 6,a (t 5 ) + p) with p = ∆ 6,a (t ). The reason for subtracting the probability that t 6 reaches t after performing a is that t |= b 1 .

We conclude by observing that focussing on t as derivative with the minimum Φ ∨ -set is indeed problematic, because it would result in a 0.5 b 1 when considering t as derivative of t 5 , but it would result in a 0.5 ( b 1 ∨ c 1 ) when considering t as derivative of t 6 , with the latter formula not distinguishing be-tween t 5 and t 6 . Moreover, when focussing on t 5 , no formula φ could have been found such that t 5 |= φ =| t as Φ ∨ (t ) Φ ∨ (t 5 ).

The last example shows that, in the general format a 1−(∆2,a(t )+p) j∈J φ 2,j for the PML ∨ distinguishing formula mentioned at the beginning of this subsection, the set J only contains any derivative of the second node different from t 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 t . Furthermore, the value p is the probability that the second node reaches the excluded derivatives that do not satisfy j∈J φ 2,j ; note 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 t 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 t 9 and t 10 in Fig. 1(e), we have: where ∆ 9,a (t ) = ∆ 9,a (t ) = 0.5, ∆ 10,a (t ) = ∆ 10,a (t ) = 0.4, ∆ 10,a (t 10 ) = ∆ 10,a (t 10 ) = 0.1, and ∆ 9,a (t 10 ) = ∆ 9,a (t 10 ) = 0, we have:

Φ ∨ (t 9 ) = { a 1 , a 0.5 b 1 , a 0.5 c 1 } Φ ∨ (t 10 ) = { a 1 ,Φ ∨ (t ) = { b 1 , c 1 } Φ ∨ (t ) = ∅ Φ ∨ (t 10 ) = { b 1 } Φ ∨ (t 10 ) = { c 1 }

If we focus on t because ∆ 9,a (t ) > ∆ 10,a (t ) and its Φ ∨ -set is minimal, then

t |= b 1 =| t with b 1 ∈ Φ ∨ (t ) \ Φ ∨ (t ), t |= b 1 =| t 10 with b 1 ∈ Φ ∨ (t 10 ) \ Φ ∨ (t )

, and t |= c 1 =| t 10 with c 1 ∈ Φ ∨ (t 10 )\Φ ∨ (t ). Thus, t 9 |= a 0.6 ( b 1 ∨ c 1 ) =| t 10 where the formula belongs to Φ ∨ (t 10 ) and the value 0.6 decorating the a-diamond stems from 1 − ∆ 10,a (t ).

If ∨ were used in place of ∨, then in Φ ∨ (t 10 ) we would also have formulas like a 0.5 ( b 1 ∨ b 1 ) and a 0.5 ( c 1 ∨ c 1 ). These are useless in that logically equivalent to other formulas already in Φ ∨ (t 10 ) in which disjunction does not occur and, most importantly, would apparently augment the size of Φ ∨ (t 10 ), an inappropriate fact in the case that t 10 were a derivative of some other node instead of being the root of a tree.

If hplb were not used, then in Φ ∨ (t 10 ) we would also have formulas like a 0.1 b 1 , a 0.4 b 1 , a 0.1 c 1 , and a 0.4 c 1 , in which the probabilistic lower bounds of the a-diamonds are not maximal with respect to the satisfiability of formulas of that form by t 10 ; those with maximal probabilistic lower bounds associated with a-diamonds are a 0.5 b 1 and a 0.5 c 1 , which already belong to Φ ∨ (t 10 ). In the case that t 9 and t 10 were derivatives of two nodes under comparison instead of being the roots of two trees, the presence of those additional formulas in Φ ∨ (t 10 ) may lead to focus on t 10 instead of t 9 -for reasons that will be clear in Ex. 8 -thereby producing no distinguishing formula.

Example 7. For the nodes t 11 , t 12 , t 13 in Fig. 1(f), we have:

Φ ∨ (t 11 ) = { a 1 } Φ ∨ (t 12 ) = { a 1 , a 1 b 1 } Φ ∨ (t 13 ) = { a 1 , a 0.7 b 1 }

Let us view them as derivatives of other nodes, rather than roots of trees. The presence of formula a 1 in Φ ∨ (t 12 ) and Φ ∨ (t 13 ) -although it has not the maximum number of nested diamonds in those two sets -ensures the minimality of Φ ∨ (t 11 ) and hence that t 11 is selected for building a distinguishing formula. If a 1 were not in Φ ∨ (t 12 ) and Φ ∨ (t 13 ), then t 12 and t 13 could be selected, but no distinguishing formula satisfied by t 11 could be obtained.

The criterion for selecting the right t 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 t 5 and t 6 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 t 6 because Φ ∨ (t 6 ) contains fewer formulas. However, by so doing, we would be unable to find a distinguishing formula in Φ ∨ (t 5 ) that is not satisfied by t 6 . Indeed, if we look carefully at the formulas without disjunctions in Φ ∨ (t 5 ) and Φ ∨ (t 6 ), we note that they differ only for their probabilistic lower bounds:

a 1 ∈ Φ ∨ (t 6

) is a variant of a 1 ∈ Φ ∨ (t 5 ), a 0.5 b 1 ∈ Φ ∨ (t 6 ) is a variant of a 0.25 b 1 ∈ Φ ∨ (t 5 ), and a 0.5 c 1 ∈ Φ ∨ (t 6 ) is a variant of a 0.25 c 1 ∈ Φ ∨ (t 5 ). Therefore, we must focus on t 5 because Φ ∨ (t 5 ) contains formulas without disjunctions such as a 0.25 b 1 and a 0.25 c 1 having smaller bounds: Φ ∨ (t 5 ) is a (≤, <)-variant of Φ ∨ (t 6 ).

Consider now the nodes t 9 and t 10 in Fig. 1(e), whose Φ ∨ -sets are shown in Ex. 6. If function hplb were not used and hence Φ ∨ (t 10 ) also contained a 0.1 b 1 , Theorem 7. Let (T, A, −→) be in RPT f and t 1 , t 2 ∈ T . Then t 1 = t 2 iff t 1 |= φ ⇐⇒ t 2 |= φ for all φ ∈ PML ∧ . Moreover, if t 1 = t 2 , then there exists φ ∈ PML ∧ distinguishing t 1 from t 2 such that depth(φ) ≤ max(height(t 1 ), height(t 2 )).

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 simulation 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 distinguishing 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.