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.