Larsen and Skou characterized probabilistic bisimilarity over reactive probabilistic systems with a logic including true, negation, conjunction, and a diamond modality decorated with a probabilistic lower bound. Later on, Desharnais, Edalat, and Panangaden showed that negation 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 reactive 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.
Since its introduction [
Later on, Desharnais, Edalat, and Panangaden [
Copyright c by the paper’s authors. Copying permitted for private and academic purposes.
In this paper, we show that ∨ can be used in place of ∧ without having to reintroduce negation: the constructs >, ∨, and haip 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 [
2.1
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 [
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 a add up to 1. As usual, we denote (s, a, Δ) ∈ −→ as s −→ Δ, where the set of reachable states coincides with supp(Δ). We also define cumulative reachability as Δ(S0) = Ps0∈S0 Δ(s0) for all S0 ⊆ S.
Probabilistic bisimilarity for the class of reactive probabilistic processes was
introduced by Larsen and Skou [
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 [
Larsen and Skou [
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 correa 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 [
BRP is finitary (because we restrict to finitely supported distributions) and
hence admits final coalgebra (cf. [
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 [
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 (·)|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 “relational” format. We define a functor D0 : Set → Set as follows: D0X , {∅}∪{U ∈Pf (X×R(0,1]) | P(x,p)∈U p = 1 and (x, p), (x, q) ∈ U ⇒ p = q} D0f , λU ∈ D0X.{(f (x), P(x,p)∈U p) | x ∈ π1(U )} for any f : X → Y. Proposition 3. D0A =∼ BRP , and Coalg(D0A) =∼ Coalg(BRP ); hence the (supports of the) final D0A-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. t1|n = t2|n.
S: s1 ∼PB s2 iff Js1K = Js2K.
Theorem 3 (Compactness). For all t1, t2 ∈ RPT: t1 = t2 iff for all n ∈ N : Corollary 1. Let (S, A, −→) be an RPLTS. For all s1, s2 ∈ S: s1 ∼PB s2 iff for all n ∈ N : Js1K|n = Js2K|n. 4
∨ 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.
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 [
Moreover, we redemonstrate Desharnais, Edalat, and Panangaden’s result for
PML∧ through yet another adaptation of the proof scheme that, unlike the proof
in [
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¬∧, it would suffice to consider ¬φ02,j .
As a consequence, t1 |= haiΔ1,a(t0) Vj φ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 probabilistic lower bound for which t1 satisfies such a formula, because Vj φ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)).
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 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 otherwise, thanks to the presence of negation in PML¬∨, it would suffice to consider ¬φ02,j . Therefore, t1 6|= hai1−Δ2,a(t0) Wj φ02,j =| t2 because 1−Δ2,a(t0) > 1−Δ1,a(t0) 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)). 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 t1 6|= hai1−(Δ2,a(t0)+p) Wj∈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 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 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 t1 a 0.5t’’ t’0.4 b c 0.4
0.1 t’’ t1’’0’ b 0.1t’’’’
10 c 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 discriminating 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: – 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 Wh∈H hahiph φ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) = ∅. – If height(t) ≥ 1 for t having transitions of the form t −a→i Δi with supp(Δi) = {t0i,j | j ∈ Ji} and i ∈ I 6= ∅, then:.Φ∨(t) = {haii1 | i ∈ I} ∪
S iS∈I hplb(∅6=J0⊆Ji{haiijP∈J0 Δi(t0i,j) j∈WJ0 φ0i,j,k | t0i,j ∈ supp(Δi), φ0i,j,k ∈ Φ∨(t0i,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 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, hai1hbi1} Φ∨(t8) = {hai1, hai1hbi1, hai1hci1} 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 hai1hci1 ∈ Φ∨(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 t07 because Δ7,a(t07) > Δ8,a(t07) and its Φ∨-set is minimal, then t07 6|= hci1 =| t08 with hci1 ∈ Φ∨(t08) \ Φ∨(t07). As a consequence, t7 6|= hai1hci1 =| t8 where the value 1 decorating the a-diamond stems from 1 − Δ8,a(t07). Example 4. For the nodes t1 and t2 in Fig. 1(a), we have: Φ∨(t1) = {hai1, hai0.5hbi1, hai0.5hci1} Φ∨(t2) = {hai1, hai0.5hbi1, hai0.5hci1, hai1 (hbi1 ∨ hci1)} The formulas with two diamonds and no disjunction are identical in the two sets, so their disjunction hai0.5hbi1 ∨ hai0.5hci1 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 t1 −a→ Δ1,a and t2 −a→ Δ2,a where Δ1,a(t01) = Δ1,a(t010) = 0.5 = Δ2,a(t02) = Δ2,a(t020) and Δ1,a(t02) = Δ1,a(t020) = 0 = Δ2,a(t01) = Δ2,a(t010), we have: Φ∨(t01) = {hbi1, hci1} Φ∨(t010) = ∅ Φ∨(t02) = {hbi1} Φ∨(t020) = {hci1} If we focus on t010 because Δ1,a(t010) > Δ2,a(t010) and its Φ∨-set is minimal, then t010 6|= hbi1 =| t02 with hbi1 ∈ Φ∨(t02) \ Φ∨(t010) as well as t010 6|= hci1 =| t020 with hci1 ∈ Φ∨(t020)\Φ∨(t010). Thus, t1 6|= hai1 (hbi1 ∨hci1) =| t2 where value 1 decorating the a-diamond stems from 1 − Δ2,a(t010).
Example 5. For the nodes t5 and t6 in Fig. 1(c), we have: Φ∨(t5) = {hai1, hai0.25hbi1, hai0.25hci1, hai0.5 (hbi1 ∨ hci1)} Φ∨(t6) = {hai1, hai0.5hbi1, hai0.5hci1} 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.5hbi1 ∈ Φ∨(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(t0500) = 0.25, Δ5,a(t00) = 0.5 = Δ6,a(t06) = Δ6,a(t00), and Δ5,a(t06) = 0 = Δ6,a(t05) = Δ6,a(t0500), we have:
Φ∨(t05) = {hbi1} Φ∨(t0500) = {hci1} Φ∨(t06) = {hbi1, hci1} Φ∨(t00) = ∅ Notice that t00 might be useless for discriminating purposes because it has the same probability in both distributions, so we exclude it. If we focus on t0500 because Δ5,a(t0500) > Δ6,a(t0500) and its Φ∨-set is minimal after the exclusion of t00, then t0500 6|= hbi1 =| t06 with hbi1 ∈ Φ∨(t06) \ Φ∨(t0500), 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.5hbi1 =| t6 where the value 0.5 decorating the a-diamond stems from 1 − (Δ6,a(t0500) + p) with p = Δ6,a(t00). The reason for subtracting the probability that t6 reaches t00 after performing a is that t00 6|= hbi1.
We conclude by observing that focussing on t00 as derivative with the minimum Φ∨-set is indeed problematic, because it would result in hai0.5hbi1 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 between t5 and t6. Moreover, when focussing on t0500, no formula φ0 could have been found such that t0500 6|= φ0 =| t00 as Φ∨(t00) ( Φ∨(t0500).
The last example shows that, in the general format hai1−(Δ2,a(t0)+p) Wj∈J φ02,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 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 Wj∈J φ02,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 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.5hbi1, hai0.5hci1} Φ∨(t10) = {hai1, hai0.5hbi1, hai0.5hci1, 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(t01000) = Δ10,a(t010000) = 0.1, and Δ9,a(t01000) = Δ9,a(t010000) = 0, we have:
Φ∨(t0) = {hbi1, hci1} Φ∨(t00) = ∅ Φ∨(t01000) = {hbi1} Φ∨(t010000) = {hci1} If we focus on t00 because Δ9,a(t00) > Δ10,a(t00) and its Φ∨-set is minimal, then t00 6|= hbi1 =| t0 with hbi1 ∈ Φ∨(t0) \ Φ∨(t00), t00 6|= hbi1 =| t01000 with hbi1 ∈ Φ∨(t01000) \ Φ∨(t00), and t00 6|= hci1 =| t010000 with hci1 ∈ Φ∨(t010000)\Φ∨(t00). 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.1hbi1, hai0.4hbi1, hai0.1hci1, and hai0.4hci1, 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.5hbi1 and hai0.5hci1, which already belong to Φ∨(t10). In the case that t9 and t10 were derivatives of two nodes under 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, hai1hbi1} Φ∨(t13) = {hai1, hai0.7hbi1} 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 maximum 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.5hbi1 ∈ Φ∨(t6) is a variant of hai0.25hbi1 ∈ Φ∨(t5), and hai0.5hci1 ∈ Φ∨(t6) is a variant of hai0.25hci1 ∈ Φ∨(t5). Therefore, we must focus on t5 because Φ∨(t5) contains formulas without disjunctions such as hai0.25hbi1 and hai0.25hci1 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.1hbi1, hai0.4hbi1, hai0.1hci1, and hai0.4hci1, 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) Wj∈J φ02,j, 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)).
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 Vj∈J φ02,j 6=| t2. For any node t of 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 transitions 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 transitions considered for that node. Given t having transitions of the form t −a→i Δi with supp(Δi) = {t0i,j | j ∈ Ji} and i ∈ I 6= ∅, we let: Φ∧(t) = {haii1 | i ∈ I} ∪ S splb({| haiiΔi(t0i,j) k∈VK0 φ0i,j,k | ∅ 6= K0 ⊆ Ki,j, t0i,j ∈ supp(Δi), φ0i,j,k ∈ Φ∧(t0i,j) |}) i∈I 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 Vj∈J φ02,j. Finally, when selecting t0, we have to leave out all the derivatives whose Φ∧-sets have (≤, <)-variants. 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
In this paper, we have studied modal logic characterizations of strong bisimilarity
over reactive probabilistic processes. Starting from previous work by Larsen and
Skou [
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 [