Characterising Probabilistic Processes Logically

(Extended Abstract)

Yuxin Deng^{1}^{,}^{2}^{⋆} and Rob van Glabbeek^{3}^{,}^{4}

1 Dept. Comp. Sci. & Eng. and MOE-Microsoft Key Lab for Intell. Comp. & Syst.,

Shanghai Jiao Tong University, China

2 State Key Lab of Comp. Sci., Inst. of Software, Chinese Academy of Sciences

3 NICTA, Australia 4 University of New South Wales, Australia

Abstract. In this paper we work on (bi)simulation semantics of processes that exhibit both nondeterministic and probabilistic behaviour. We propose a probabilistic extension of the modal mu-calculus and show how to derive characteristic formulae for various simulation-like preorders over finite-state processes without divergence. In addition, we show that even without the fixpoint operators this probabilistic mu-calculus can be used to characterise these behavioural relations in the sense that two states are equivalent if and only if they satisfy the same set of formulae.

1 Introduction

In concurrency theory, behavioural relations such as equivalences and refinement preorders form a basis for establishing system correctness. Usually both specifications and implementations are expressed as processes within the same framework, in which a specification describes some high-level behaviour and an implementation gives the technical details for achieving the behaviour. Then one chooses an equivalence or preorder to verify that the implementation realises the behaviour required by the specification.

A great many behavioural relations are defined on top of labelled transition systems, which offer an operational model of systems. For finitary (i.e. finite-state and finitely branching) systems, these behavioural relations can be computed in a mechanical way, and thus may be incorporated into automatic verification tools. In recent years, probabilistic constructs have been proven useful for giving quantitative specifications of system behaviour. The first papers on probabilistic concurrency theory [12,2,20] proceed by replacing nondeterministic with probabilistic constructs. The reconciliation of nondeterministic and probabilistic constructs starts with [13] and has received a lot of attention in the literature [35,31,21,30,16,22,1,18,25,3,34,23,9,7,4]. We shall also work in a framework that features the co-existence of probability and nondeterminism.

Among the behavioural relations that have proven useful in probabilistic concurrency theory are various types of simulation and bisimulation relations. Axiomatisations for bisimulations have been investigated in [1,10]. Logical characterisations of bisimulations and simulations have been studied in [31,27]. For

⋆ Deng was supported by the National Natural Science Foundation of China (60703033).

example, in [31] the probabilistic computation tree logic (PCTL) [14] is used and it turns out that two states are bisimilar if and only if they satisfy the same set of PCTL formulae.

In the nonprobabilistic setting, there is a line of research on characteristic formulae. The goal is to seek a particular formula φ_{s} for a given state s such that a necessary and sufficient condition for any state t being bisimilar to s is to satisfy φ_{s} [32]. This is a very strong property in the sense that to check if t is bisimilar to s it suffices to consider the single formula φ_{s} and see if it can be satisfied by t. It offers a convenient method for equivalence or preorder checking.

In this paper we partially extend the results of [32] to a probabilistic setting that admits both probabilistic and nondeterministic choice; to make the main ideas neat we do not consider divergence. We present a probabilistic extension of the modal mu-calculus [19] (pMu), where a formula is interpreted as the set of probability distributions satisfying it. This is in contrast to the probabilistic semantics of the mu-calculus as studied in [16,22,23] where formulae denote lower bounds of probabilistic evidence of properties, and the semantics of the generalised probabilistic logic of [3] where a mu-calculus formula is interpreted as a set of deterministic trees that satisfy it.

We shall provide characteristic formulae for strong and weak probabilistic (bi)simulation as introduced in [31,30], as well as forward simulation [30] and failure simulation [7]. The results are obtained in two phases, which we illustrate by taking strong probabilistic bisimilarity ∼ as an example. Given a finite-state probabilistic labelled transition system with state space {s_{1}, ..., s_{n}}, we first construct an equation system E of modal formulae in pMu.

E : X_{s_{1}} = φ_{s_{1}} ; ⋮ ; X_{s_{n}} = φ_{s_{n}}

A solution of the equation system is a function ρ that assigns to each variable X_{s_{i}} a set of distributions ρ(X_{s_{i}}). The greatest solution of the equation system, denoted by ν_{E}, has the property that s_{i} ∼ s_{j} if and only if the point distribution \overline{s_{j}} is an element of ν_{E}(X_{s_{i}}). In the second phase, we apply three transformation rules upon E in order to obtain a pMu formula φ_{s_{i}}^{∼} whose meaning [[φ_{s_{i}}^{∼}]] is exactly captured by ν_{E}(X_{s_{i}}). As a consequence, we derive a characteristic formula for s_{i} such that s_{i} ∼ s_{j} if and only if \overline{s_{j}} ∈ [[φ_{s_{i}}^{∼}]].

Without the fixpoint operators pMu gives rise to a probabilistic extension of the Hennessy-Milner logic [15]. In analogy to the nonprobabilistic setting, it characterises (bi)simulations in the sense that s ∼ t if and only if the two states s, t satisfy the same set of formulae.

The paper is organised as follows. In Section 2 we recall the definitions of several (bi)simulations defined over probabilistic labelled transition systems. In Section 3 we introduce the syntax and semantics of pMu. In Section 4 we build characteristic equation systems and derive from them characteristic formulae for all our (bi)simulations. In Section 5 we consider the fixpoint-free fragment of pMu which characterises a state by the class of formulae it satisfies.

In this extended abstract many proofs are omitted; they can be found in [6].

2 Probabilistic (bi)simulations

In this section we recall several probabilistic extensions of simulation and bisimulation [24] that appeared in the literature.

We begin with some notation concerning probability distributions. A (discrete) probability distribution over a set S is a function Δ : S → [0, 1] with ∑_{s∈S}Δ(s) = 1; the support of Δ is given by ⌈Δ⌉ = { s ∈ S | Δ(s) > 0 }. We write D(S), ranged over by Δ, Θ, for the set of all distributions over S. We also write \overline{s} to denote the point distribution assigning probability 1 to s and 0 to all others, so that ⌈\overline{s}⌉ = \{s\}. If p_{i} ≥ 0 and Δ_{i} is a distribution for each i in some index set I, and ∑_{i∈I} p_{i} = 1, then the probability distribution ∑_{i∈I} p_{i} · Δ_{i} ∈ D(S) is given by (∑_{i∈I} p_{i} · Δ_{i})(s) = ∑_{i∈I} p_{i} · Δ_{i}(s); we will sometimes write it as p_{1} · Δ_{1} + … + p_{n} · Δ_{n} when I = {1, …, n}.

Definition 1. A finite state probabilistic labelled transition system (pLTS) is a triple ⟨S, Act_{τ} , →⟩, where

1. S is a finite set of states

2. Act_{τ} is a set of external actions Act augmented with an internal action τ ∉Act 3. → ⊆ S × Act_{τ} × D(S).

We usually write s ⟶^{a} Δ for (s, a, Δ) ∈ →, s ⟶^{a} for ∃Δ : s ⟶^{a} Δ, and s −̸→^{a} for the negation of s ⟶^{a}. We write s −̸→^{A} with A ⊆ Act when ∀a ∈ A ∪ {τ} : s −̸→^{a}, and Δ −̸→^{A} when ∀s ∈ ⌈Δ⌉ : s −̸→^{A}. A pLTS is finitely branching if, for each state s, the set {(a, Δ) | s ⟶^{a} Δ} is finite. A pLTS is finitary if it is finite-state and finitely branching.

To define probabilistic (bi)simulations, it is often necessary to lift a relation over states to one over distributions.

Definition 2. Given two sets S and T and a relation R ⊆ S × T. We lift R to a relation R^{†} ⊆ D(S) × D(T) by letting Δ R^{†} Θ whenever

1. Δ = ∑_{i∈I} p_{i} · \overline{s_{i}}, where I is a countable index set and ∑_{i∈I} p_{i} = 1

2. for each i ∈ I there is a state t_{i} such that s_{i} R t_{i}

3. Θ = ∑_{i∈I} p_{i} · \overline{t_{i}}.

Note that in the decomposition of Δ, the states s_{i} are not necessarily distinct: that is, the decomposition is not in general unique, and similarly for the decomposition of Θ. For example, if R = {(s_{1}, t_{1}), (s_{1}, t_{2}), (s_{2}, t_{3}), (s_{3}, t_{3})}, Δ = \frac{1}{2} \overline{s_{1}} + \frac{1}{4} \overline{s_{2}} + \frac{1}{4} \overline{s_{3}}, and Θ = \frac{1}{3} \overline{t_{1}} + \frac{1}{6} \overline{t_{2}} + \frac{1}{2} \overline{t_{3}}, then Δ R^{†} Θ holds because of the decompositions Δ = \frac{1}{3} \overline{s_{1}} + \frac{1}{6} \overline{s_{1}} + \frac{1}{4} \overline{s_{2}} + \frac{1}{4} \overline{s_{3}} and Θ = \frac{1}{3} \overline{t_{1}} + \frac{1}{6} \overline{t_{2}} + \frac{1}{4} \overline{t_{3}} + \frac{1}{4} \overline{t_{3}}.

From the above definition, the next two properties follow [5]. In fact, they are sometimes used as alternative methods of lifting relations (see e.g. [31,20]).

Proposition 1. 1. Let Δ and Θ be distributions over S and T, respectively. Then Δ R^{†} Θ iff there exists a weight function w : S × T → [0, 1] such that (a) ∀s ∈ S : ∑_{t∈T} w(s, t) = Δ(s)

(b) ∀t ∈ T : ∑_{s∈S} w(s, t) = Θ(t)

(c) ∀(s, t) ∈ S × T : w(s, t) > 0 ⇒ s R t.

2. Let Δ, Θ be distributions over S and R be an equivalence relation. Then Δ R^{†} Θ iff Δ(C) = Θ(C) for all equivalence classes C ∈ S/R, where Δ(C) stands for the accumulated probability ∑_{s∈C} Δ(s). ⊓ ⊔

In a similar way, following [9], we can lift a relation R ⊆ S × D(T) to a relation R^{†} ⊆ D(S) × D(T), by letting Δ R^{†} Θ whenever

1. Δ = ∑_{i∈I} p_{i} · \overline{s_{i}}, where I is a countable index set and ∑_{i∈I} p_{i} = 1

2. for each i ∈ I there is a distribution Θ_{i} such that s_{i} R Θ_{i}

3. Θ = ∑_{i∈I} p_{i} · Θ_{i}.

The above lifting constructions satisfy the following two useful properties.

Proposition 2. Suppose R ⊆ S × S or S × D(S) and ∑_{i∈I} p_{i} = 1. Then

1. Δ_{i} R^{†} Θ_{i} for all i ∈ I implies (∑_{i∈I} p_{i} · Δ_{i}) R^{†} (∑_{i∈I} p_{i} · Θ_{i}).

2. If (∑_{i∈I} p_{i} · Δ_{i}) R^{†} Θ then Θ = ∑_{i∈I} p_{i} · Θ_{i} for some set of distributions Θ_{i} such that Δ_{i} R^{†} Θ_{i} for all i ∈ I. ⊓ ⊔

We write s ⟶^{τ̂} Δ if either s ⟶^{τ} Δ or Δ = \overline{s}, and s ⟶^{â} Δ iff s ⟶^{a} Δ for a ∈ Act. For any a ∈ Act_{τ}, we know that ⟶^{â} ⊆ S × D(S), so we can lift it to be a transition relation between distributions. With a slight abuse of notation we simply write Δ ⟶^{â} Θ for Δ (⟶^{â})^{†} Θ. Then we define weak transitions ⟹^{â} by letting ⟹^{τ̂} be the reflexive and transitive closure of ⟶^{τ̂} and writing Δ ⟹^{â} Θ for a ∈ Act whenever Δ ⟹^{τ̂}⟶^{â}⟹^{τ̂} Θ.

Definition 3. A divergence is a sequence of states s_{i} and distributions Δ_{i} with

s_{i} ⟶^{τ} Δ_{i} and s_{i+1} ∈⌈Δ_{i}⌉ for i ≥ 0.

The above definition of ⟹^{â} is sensible only in the absence of divergence. In general, one would need a more complicated notion of ⟹^{â}, such as proposed in [8]. Therefore, from here on we restrict attention to divergence-free pLTSs.

Definition 4. A relation R ⊆ S × S is a strong probabilistic simulation if s R t and a ∈ Act_{τ} implies

– if s ⟶^{a} Δ then there exists some Θ such that \overline{t} ⟶^{a} Θ and Δ R^{†} Θ

If both R and R^{−1} are strong probabilistic simulations, then R is a strong probabilistic bisimulation. A state s is related to another state t via strong probabilistic similarity (resp. bisimilarity), denoted s ≺ t (resp. s ∼ t), if there exists a strong probabilistic simulation (resp. bisimulation) R such that s R t. Weak probabilistic similarity (≾) and weak probabilistic bisimilarity (≈) are defined in the same manner just by using \overline{t} ⟹^{â} Θ in place of \overline{t} ⟶^{a} Θ.

All four (bi)simulations above stem from [31,30]. There they were proposed as improvements over the strong bisimulation of [13] and the strong simulation of [17], both of which can be defined as the strong probabilistic (bi)simulation above, but using t ⟶^{a} Θ in place of \overline{t} ⟶^{a} Θ. Logical characterisations for strong (bi)simulations are similar to those contributed here for strong probabilistic (bi)simulations, but require a state-based interpretation of the modalities ⟨a⟩ and [a]; see [6] for details. Other definitions of simulation have also appeared in the literature. Here we consider two typical ones: forward simulation [30] and failure simulation [7].

Definition 5. A relation R ⊆ S × D(S) is a failure simulation if s R Θ implies 1. if s ⟶^{a} Δ with a ∈ Act_{τ} then ∃Θ′ such that Θ ⟹^{â} Θ′ and Δ R^{†} Θ′;

2. if s −̸→^{A} with A ⊆ Act then ∃Θ′ such that Θ ⟹^{τ̂} Θ′ and Θ′ −̸→^{A}. We write s ◁_{FS} Θ if there is some failure simulation R such that s R Θ.

Similarly, we define a forward simulation and s ◁_{S} Θ by dropping the second clause in Definition 5.

3 The Probabilistic Modal mu-Calculus

Let Var be a countable set of variables. We define a class L^{raw} of modal formulae by the following grammar:

φ := ⋀_{i∈I} φ_{i} | ⋁_{i∈I} φ_{i} | ¬φ | ⟨a⟩φ | [a]φ | ⨁_{i∈I} φ_{i} | ⨁_{i∈I} p_{i} · φ_{i} | ↓φ | X | μX.φ | νX.φ

where I is an index set, a ∈ Act_{τ} and ∑_{i∈I} p_{i} = 1. The probabilistic modal mucalculus (pMu) is given by the subclass L, obtained by imposing the syntactic condition that in μX.φ and νX.φ the variable X may occur in φ only within the scope of an even number of negations. The above syntax is obtained by adding a variant of the probabilistic construct ⨁_{i∈I} p_{i} · φ_{i}, introduced in [7] in the context of a less expressive logic without fixpoint operators, as well as the novel modalities ⨁_{i∈I} φ_{i} and ↓φ, to the syntax of the non-probabilistic mu-calculus [19]. As usual, one has ⋀_{i∈∅} φ_{i} = true and ⋁_{i∈∅} φ_{i} = false.

The two fixpoint operators μX and νX bind the respective variable X. We apply the usual terminology of free and bound variables in a formula and write fv(φ) for the set of free variables in φ. A formula φ is closed if fv(φ) = ∅.

For any set Ω, write 𝒫(Ω) for the power set of Ω. We use environments, which bind free variables to sets of distributions, in order to give semantics to formulae. Let

Env = { ρ | ρ : Var → 𝒫(D(S)) }

be the set of all environments and ranged over by ρ. For a set V ⊆ D(S) and a variable X ∈ Var, we write ρ[X ↦ V] for the environment that maps X to V and Y to ρ(Y) for all Y ≠ X.

The semantics of a formula φ in an environment ρ is given as the set of distributions [[φ]]_{ρ} satisfying it. This leads to a semantic functional [[ ]] : L → Env → 𝒫(D(S)) defined inductively in Table 1. As the meaning of a closed formula φ does not depend on the environment, one writes [[φ]] for [[φ]]_{ρ} where ρ is an arbitrary environment. In that case one also writes Δ ⊧ φ for Δ ∈ [[φ]].

Following [19,29] we give a strong and a weak semantics of the probabilistic modal mu-calculus. Both are the same as those of the modal mu-calculus [19,29] except that distributions of states are taking the roles of states. The power set of D(S), 𝒫(D(S)), may be viewed as the complete lattice (𝒫(D(S)), D(S), ∅, ⊆, ∪, ∩). Intuitively, we identify a formula with the set of distributions that make it true. For example, true holds for all distributions and dually false

[[⋀_{i∈I} φ_{i}]]_{ρ} = ⋂_{i∈I}[[φ_{i}]]_{ρ}  so  [[true]]_{ρ} = D(S)
[[⋁_{i∈I} φ_{i}]]_{ρ} = ⋃_{i∈I}[[φ_{i}]]_{ρ}  so  [[false]]_{ρ} = ∅
[[¬φ]]_{ρ} = D(S) \ [[φ]]_{ρ}
[[⟨a⟩φ]]_{ρ} = { Δ ∈ D(S) | ∃Δ′ : Δ ⟶^{a} Δ′ ∧ Δ′ ∈ [[φ]]_{ρ} }
[[[a]φ]]_{ρ} = { Δ ∈ D(S) | ∀Δ′ : Δ ⟶^{a} Δ′ ⇒ Δ′ ∈ [[φ]]_{ρ} }
[[⨁_{i∈I} φ_{i}]]_{ρ} = \{ Δ ∈ D(S) | \begin{matrix}Δ = ∑_{i∈I} p_{i} · Δ_{i} for some p_{i} with ∑_{I∈I} p_{i} = 1 \\ ∧ ∀i ∈ I : Δ_{i} ∈ [[φ_{i}]]_{ρ} \} \end{matrix}
[[⨁_{i∈I} p_{i} · φ_{i}]]_{ρ} = { Δ ∈ D(S) | Δ = ∑_{i∈I} p_{i} · Δ_{i} ∧ ∀i ∈ I : Δ_{i} ∈ [[φ_{i}]]_{ρ} }
[[↓φ]]_{ρ} = \{ Δ ∈ D(S) | ∀s ∈ ⌈Δ⌉ : \overline{s} ∈ [[φ]]_{ρ} \}
[[X]]_{ρ} = ρ(X)
[[μX.φ]]_{ρ} = ⋂{ V ⊆ D(S) | [[φ]]_{ρ[X↦V ]} ⊆ V }
[[νX.φ]]_{ρ} = ⋃{ V ⊆ D(S) | [[φ]]_{ρ[X↦V ]} ⊇ V }
[[⟨a⟩φ]]_{ρ} = { Δ ∈ D(S) | ∃Δ′ : Δ ⟹^{â} Δ′ ∧ Δ′ ∈ [[φ]]_{ρ} }
[[[a]φ]]_{ρ} = { Δ ∈ D(S) | ∀Δ′ : Δ ⟹^{â} Δ′ ⇒ Δ′ ∈ [[φ]]_{ρ} }

Table 1. Strong and weak semantics of the probabilistic modal mu-calculus

holds for no distribution. Conjunction and disjunction are interpreted by intersection and union of sets, and negation by complement. The formula ⟨a⟩φ holds for a distribution Δ if there is a distribution Δ′ that can be reached after an a-transition and that satisfies φ. Dually, [a]φ holds for Δ if all distributions reachable from Δ by an a-transition satisfy φ. The formulas ⨁_{i∈I} φ_{i} and ⨁_{i∈I} p_{i} · φ_{i} hold for Δ if the distribution can be decomposed into a convex combination of some distributions Δ_{i} and each of them satisfies the corresponding sub-formula φ_{i}; the first of these modalities allows any convex combination, whereas the second one specifies a particular one. The formula ↓φ holds for Δ if all states in its support satisfy φ. The characterisation of the least fixpoint formula μX.φ and the greatest fixpoint formula νX.φ follows from the well-known Knaster-Tarski fixpoint theorem [33].

The weak semantics reflects the unobservable nature of internal actions; it differs from the strong semantics only in the use of the relations ⟹^{â} instead of ⟶^{a} in the interpretation of the modalities ⟨a⟩ and [a].

Note that there is some redundancy in the syntax of pMu: each of the constructs ⋀_{i∈I}, ⟨a⟩ and μ can be expressed in terms of its dual ⋁_{i∈I}, [a] and ν with the aid of negation. However, negation may not be redundant, as the dual of ⨁_{i∈I} p_{i} · φ_{i} does not appear to be expressible without using negation; moreover this dual lacks the intuitive appeal for introducing it as a new primitive.

We shall consider (closed) equation systems of formulae of the form

E : X_{1} = φ_{1} ; ⋮ ; X_{n} = φ_{n}

where X_{1}, ..., X_{n} are mutually distinct variables and φ_{1}, ..., φ_{n} are formulae having at most X_{1}, ..., X_{n} as free variables. Here E can be viewed as a function

– Rule 1: E → F

– Rule 2: E → G

– Rule 3: E → H if X_{n} ∉ fv(φ_{1}, ..., φ_{n})

\begin{aligned}E : & X_{1} & = & φ_{1} & F : & X_{1} & = & φ_{1} & G : & X_{1} & = & φ_{1}[φ_{n}/X_{n}] & H : & X_{1} & = & φ_{1} \\ & ⋮ & & & ⋮ & & & ⋮ & & & ⋮ \\ X_{n−1} & = & φ_{n−1} & X_{n−1} & = & φ_{n−1} & X_{n−1} & = & φ_{n−1}[φ_{n}/X_{n}] & X_{n−1} & = & φ_{n−1} \\ X_{n} & = & φ_{n} & X_{n} & = & νX_{n}.φ_{n} & X_{n} & = & φ_{n} \end{aligned}

Table 2. Transformation rules

E : Var → L defined by E(X_{i}) = φ_{i} for i = 1, ..., n and E(Y) = Y for other variables Y ∈ Var.

An environment ρ is a solution of an equation system E if its assignment to X_{i} coincides with the interpretation of φ_{i} in the environment, that is,

∀i : ρ(X_{i}) = [[φ_{i}]]_{ρ}.

The existence of solutions for an equation system can be seen from the following arguments. The set Env, which includes all candidates for solutions, together with the partial order ⊑ defined by

ρ ⊑ ρ′ iff ∀X ∈ Var : ρ(X) ⊆ ρ′(X)

forms a complete lattice. The equation functional F_{E} : Env → Env given in the notation of the λ-calculus by

F_{E} := λρ.λX.[[E(X)]]_{ρ}

is monotonic, which can be shown by induction on the structure of E(X). Thus, the Knaster-Tarski fixpoint theorem guarantees existence of solutions, and the greatest solution

ν_{E} := ⨆{ ρ | ρ ⊑ F_{E}(ρ) }  (1)

is the supremum of the set of all post-fixpoints of F_{E}.

An expression ν_{E}(X), with X one of the variables used in E, denotes a set of distributions. Below we will use such expressions as if they were valid syntax in our probabilistic mu-calculus, with [[ν_{E}(X)]]_{ρ} := ν_{E}(X). This amounts to extending the greatest fixpoint operator ν to apply to finite sets of fixpoint equations, instead of single equations; the expression νX.φ amounts to the special case ν_{E}(X) in which E consists of the single equation X = φ.

The use of expressions ν_{E}(X) is justified because they can be seen as syntactic sugar for authentic pMu expressions. As explained in [26], the three transformation rules in Table 2 can be used to obtain from an equation system E a pMu formula whose interpretation coincides with the interpretation of X_{1} in the greatest solution of E.

Theorem 1. Given a finite equation system E that uses the variable X, there is a pMu formula φ such that ν_{E}(X) = [[φ]]. ⊓ ⊔

4 Characteristic equation systems

Following [32], the behaviour of a finite-state process can be characterised by an equation system of modal formulae. In the current section we show that this idea also applies in the probabilistic setting. For each behavioural relation R over a finite state space, ranging over the various simulation preorders and bisimulation equivalences reviewed in Section 2, we establish an equation system E of modal formulae in pMu.

E : X_{s_{1}} = φ_{s_{1}} ; ⋮ ; X_{s_{n}} = φ_{s_{n}}

There is exactly one such equation for each state s_{i}, and the formulae φ_{s_{i}} do not contain fixpoint operators. This equation system is guaranteed to have a greatest solution ν_{E} which has the nice property that, for any states s, t in the state space in question, s is related to t via R if and only if the point distribution \overline{t} belongs to the set of distributions assigned to the variable X_{s} by ν_{E}. Thus ν_{E}(X_{s}) is a characteristic formula for s w.r.t. R in the sense that s R t iff \overline{t} satisfies ν_{E}(X_{s}).

Strong probabilistic bisimulation The key ingredient for the modal characterisation of strong probabilistic bisimulation is to construct an equation system that captures all the transitions of a pLTS. For each state s we build an equation X_{s} = φ_{s}, where X_{s} is a variable and φ_{s} is of the form φ′_{s} ∧ φ′′_{s} with φ′_{s} a formula describing the actions enabled by s and φ′′_{s} a formula describing the consequences of performing these actions. Intuitively, if state s is related to state t in a bisimulation game, then φ′_{s} expresses the transitions that should be matched up by t and φ′′_{s} expresses the capability of s to match up the transitions initiated by t. More specifically, the equation system is given by the following definition.

Definition 6. Given a pLTS, its characteristic equation system for strong probabilistic bisimulation consists of one equation X_{s} = φ_{s} for each state s ∈ S, where

φ_{s} := ( ⋀_{s⟶^{a}Δ}⟨a⟩X_{Δ}) ∧ ( ⋀_{a∈Act_{τ}}[a] ⨁_{s⟶^{a}Δ} X_{Δ}) ^{1}  (2)

with X_{Δ} := ⨁_{s∈⌈Δ⌉} Δ(s) · ↓X_{s}.

The equation system thus constructed, interpreted according to the strong semantics of pMu, has the required property, as stated by the theorem below.

1 The subformula ⨁_{s⟶^{a}Δ} X_{Δ} is equivalent to ⋁_{\overline{s}⟶^{a}Δ} X_{Δ}, and this is the form that we use to prove Theorem 2. If the given pLTS has nondeterministic choices among different transitions labelled with the same action, this disjunction is infinite. For example, if s ⟶^{a} \overline{s_{i}} for i = 1, 2, then \overline{s} ⟶^{a} Δ_{p}, where Δ_{p} = p·\overline{s_{1}} +(1−p)·\overline{s_{2}}, for any p ∈ [0, 1]. The set {Δ_{p} | p ∈ [0, 1]} is uncountable, though it is finitely generable, as the convex closure of the two-element set {Δ_{0}, Δ_{1}}. The formula ⨁_{s⟶^{a}Δ} X_{Δ} exploits that fact to bypass the infinite disjunction; this formula is finite if the underlying pLTS is finitary.

Theorem 2. Let E be the characteristic equation system for strong probabilistic bisimulation on a given pLTS. Then, for all states s and t,

1. s R t for some strong probabilistic bisimulation R if and only if \overline{t} ∈ ρ(X_{s}) for some post-fixpoint ρ of F_{E}.

2. In particular, s ∼ t if and only if \overline{t} ∈ [[ν_{E}(X_{s})]], i.e., ν_{E}(X_{s}) is a characteristic formula for s w.r.t. strong probabilistic bisimilarity.

Proof. Let E be the characteristic equation system for strong probabilistic bisimulation on a given pLTS. We only consider the first statement, from which the second statement follow immediately.

(⇐) For this direction, assuming a post-fixpoint ρ of F_{E}, we construct a probabilistic bisimulation relation that includes all state pairs (s, t) satisfying \overline{t} ∈ ρ(X_{s}). Let R= \{ (s, t) | \overline{t} ∈ ρ(X_{s}) \}. We first show that

Θ ∈ [[X_{Δ}]]_{ρ} implies Δ R^{†} Θ.  (3)

Let X_{Δ} = ⨁_{i∈I} p_{i} · ↓X_{s_{i}}, so that Δ = ∑_{i∈I} p_{i} · \overline{s_{i}}. Suppose Θ ∈ [[X_{Δ}]]_{ρ}. We have that Θ = ∑_{i∈I} p_{i} · Θ_{i} and, for all i ∈ I and all t ∈⌈Θ_{i}⌉, that \overline{t} ∈ [[X_{s_{i}}]]_{ρ}, i.e. s_{i} R t. It follows that \overline{s_{i}} R^{†} Θ_{i} and thus Δ R^{†} Θ, using Proposition 2(1).

Now we show that R is a probabilistic bisimulation.

1. Suppose s R t and s ⟶^{a} Δ. Then \overline{t} ∈ ρ(X_{s}) ⊆ [[φ_{s}]]_{ρ}. It follows from (2) that \overline{t} ∈ [[⟨a⟩X_{Δ}]]_{ρ}. So there exists some Θ such that \overline{t} ⟶^{a} Θ and Θ ∈ [[X_{Δ}]]_{ρ}. Now we apply (3).

2. Suppose s R t and t ⟶^{a} Θ. Then \overline{t} ∈ ρ(X_{s}) ⊆ [[φ_{s}]]_{ρ}. It follows from (2) that \overline{t} ∈ [[[a] ⋁_{\overline{s}⟶^{a}Δ} X_{Δ}]]. Notice that it must be the case that \overline{s} ⟶^{a}, otherwise, \overline{t} ∈ [[[a]false]]_{ρ} and thus t −̸→^{a}, in contradiction with the assumption t ⟶^{a} Θ. Therefore, Θ ∈ [[⋁_{\overline{s}⟶^{a}Δ} X_{Δ}]]_{ρ}, which implies Θ ∈ [[X_{Δ}]]_{ρ} for some Δ with \overline{s} ⟶^{a} Δ. Now we apply (3).

(⇒) Given a strong probabilistic bisimulation R, we construct a post-fixpoint of F_{E} such that whenever s R t then \overline{t} falls into the set of distributions assigned to X_{s} by that post-fixpoint. We define the environment ρ_{R} by

ρ_{R}(X_{s}) := \{ \overline{t} | s R t \}

and show that ρ_{R} is a post-fixpoint of F_{E}, i.e.

ρ_{R} ⊑ F_{E}(ρ_{R}).  (4)

We first show that

Δ R^{†} Θ implies Θ ∈ [[X_{Δ}]]_{ρ_{R}}.  (5)

Suppose Δ R^{†} Θ, we have that (i) Δ = ∑_{i∈I} p_{i} · \overline{s_{i}}, (ii) Θ = ∑_{i∈I} p_{i} · \overline{t_{i}}, (iii) s_{i} R t_{i} for all i ∈ I. We know from (iii) that \overline{t_{i}} ∈ [[X_{s_{i}}]]_{ρ_{R}} and thus \overline{t_{i}} ∈ [[↓X_{s_{i}}]]_{ρ_{R}}. Using (ii) we have that Θ ∈ [[⨁_{i∈I} p_{i} ·↓X_{s_{i}}]]_{ρ_{R}}. Using (i) we obtain Θ ∈ [[X_{Δ}]]_{ρ_{R}}.

Now we are in a position to show (4). Suppose \overline{t} ∈ ρ_{R}(X_{s}). We must prove that \overline{t} ∈ [[φ_{s}]]_{ρ_{R}}, i.e.

\overline{t} ∈ ( ⋂_{s⟶^{a}Δ}[[⟨a⟩X_{Δ}]]_{ρ_{R}}) ∩ ( ⋂_{a∈Act_{τ}}[[[a] ⋁_{\overline{s}⟶^{a}Δ} X_{Δ}]]_{ρ_{R}})

by (2). This can be done by showing that \overline{t} belongs to each of the two parts of the outermost intersection.

1. Assume that s ⟶^{a} Δ for some a ∈ Act_{τ} and Δ ∈ D(S). Since s R t, there exists some Θ such that \overline{t} ⟶^{a} Θ and Δ R^{†} Θ. By (5), we get Θ ∈ [[X_{Δ}]]_{ρ_{R}}. It follows that \overline{t} ∈ [[⟨a⟩X_{Δ}]]_{ρ_{R}}.

2. Let a ∈ Act_{τ}. Whenever \overline{t} ⟶^{a} Θ, then by s R t there must be some Δ such that \overline{s} ⟶^{a} Δ and Δ R^{†} Θ. By (5), we get Θ ∈ [[X_{Δ}]]_{ρ_{R}} and thus Θ ∈ [[⋁_{\overline{s}⟶^{a}Δ} X_{Δ}]]_{ρ_{R}}. As a consequence, \overline{t} ∈ [[[a] ⋁_{\overline{s}⟶^{a}Δ} X_{Δ}]]_{ρ_{R}}. ⊓ ⊔

Strong probabilistic simulation In a simulation game, if state s is related to state t, we only need to check that all transitions initiated by s should be matched up by transitions from t, and we do not care about the inverse direction: the capability of s to simulate t. Therefore, it is not surprising that characteristic equation systems for strong probabilistic simulation are defined as in Definition 6 except that we drop the second part of the conjunction in (2), so φ_{s} takes the form

φ_{s} := ⋀_{s⟶^{a}Δ}⟨a⟩X_{Δ}  (6)

With this modification, we have the expected property for strong probabilistic simulation, which can be shown by using the ideas in the proof of Theorem 2, but with fewer cases to analyse.

Weak probabilistic bisimulation Characteristic equation systems for weak probabilistic bisimulation are defined as in Definition 6 except that the weak semantics of pMu is employed and φ_{s} takes the form

φ_{s} := ( ⋀_{s⟶^{a}Δ}⟨a⟩X_{Δ}) ∧ ( ⋀_{a∈Act_{τ}}[a] ⋁_{\overline{s}⟹^{â}Δ} X_{Δ}) ^{2}  (7)

Weak probabilistic simulation Characteristic equation systems for weak probabilistic simulation are in exactly the same form as characteristic equation systems for strong probabilistic simulation (cf. (6)), but using the weak semantics of pMu.

Forward simulation Characteristic equation systems for forward simulation are in the same form as characteristic equation systems for weak probabilistic simulation, but with X_{Δ} := ⨁_{s∈⌈Δ⌉} Δ(s) · X_{s}, i.e. dropping the ↓.

2 Using results from Markov Decision Processes [28], in a finitary pLTS also this infinite disjunction can be expressed as finite convex combination; however, we will not elaborate this here.

Failure simulation To give a modal characterisations for failure simulation we need to add modal formulae of the form ref(A) with A ⊆ Act, first introduced in [7], to pMu, with the meaning given by

[[ref(A)]]_{ρ} = { Δ ∈ D(S) | ∃Δ′ : Δ ⟹^{τ̂} Δ′ ∧ Δ′ −̸→^{A} }

The formula ref(A) holds for Δ if by doing internal actions only Δ can evolve into a distribution such that no state in its support can perform an action from A ∪ {τ}. This time φ_{s} takes the form

φ_{s} := \{ \begin{matrix}⋀_{s⟶^{a}Δ}⟨a⟩X_{Δ} & if s ⟶^{τ} \\ (⋀_{s⟶^{a}Δ}⟨a⟩X_{Δ}) ∧ ref(\{ a | s −̸→^{a} \}) & otherwise \end{matrix}  (8)

with X_{Δ} := ⨁_{s∈⌈Δ⌉} Δ(s) · X_{s}. Inspired by [7], here we distinguish two cases, depending on the possibility of making an internal transition from s.

With the above modifications, we have the counterpart of Theorem 2, with a similar proof.

Theorem 3. Let E_{≺} be the characteristic equation system for strong probabilistic simulation on a given pLTS. Let E_{≈} (E_{≾}, E_{◁_{S}}, E_{◁_{FS}}, respectively) be the characteristic equation system for weak probabilistic bisimulation (weak probabilistic simulation, forward simulation, failure simulation, respectively) on a given divergence-free pLTS. Then, for all states s, t and distributions Θ,

1. s R t for some strong probabilistic simulation (weak probabilistic bisimulation, weak probabilistic simulation, respectively) R if and only if \overline{t} ∈ ρ(X_{s}) for some post-fixpoint ρ of F_{E_{≺}} (F_{E_{≈}}, F_{E_{≾}}, respectively).

2. s R Θ for some forward simulation (failure simulation) R if and only if Θ ∈ ρ(X_{s}) for some post-fixpoint ρ of F_{E_{◁_{S}}} (F_{E_{◁_{FS}}} ).

3. In particular, (a) s ≺ t if and only if \overline{t} ∈ [[ν_{E_{≺}}(X_{s})]].

(b) s ≈ t if and only if \overline{t} ∈ [[ν_{E_{≈}}(X_{s})]].

(c) s ≾ t if and only if \overline{t} ∈ [[ν_{E_{≾}}(X_{s})]].

(d) s ◁_{FS} Θ if and only if Θ ∈ [[ν_{E_{◁_{S}}} (X_{s})]].

(e) s ◁_{FS} Θ if and only if Θ ∈ [[ν_{E_{◁_{FS}}} (X_{s})]]. ⊓ ⊔

We can also consider the strong case for ◁_{S} and ◁_{FS} by treating τ as an external action, and give characteristic equation systems. In the strong case for ◁_{FS} only the “otherwise” in (8) applies, with ref(A) represented as ⋀_{a∈A}[a]false.

5 Modal characterisations

In the previous sections we have pursued logical characterisations for various behavioural relations by characteristic formulae. A weaker form of characterisation, which is commonly called a modal characterisation of a behavioural relation, consists of isolating a class of formulae with the property that two states are equivalent if and only if they satisfy the same formulae from that class.

Definition 7. Let L_{∼}^{μ} be simply the class L of modal formulae defined in Section 3, equipped with the strong semantics of Table 1. With L_{≺}^{μ} we denote the fragment of this class obtained by skipping the modalities ¬ and [a]. The classes L_{≈}^{μ} and L_{≾}^{μ} are defined likewise, but equipped with the weak semantics. Moreover, L_{◁_{S}}^{μ} is the fragment of L_{≾}^{μ} obtained by skipping ↓, and L_{◁_{FS}}^{μ} is obtained from L_{◁_{S}}^{μ} by addition of the modality ref(A).

In all cases, dropping the superscript μ denotes the subclass obtained by dropping the variables and fixpoint operators.

For R ∈{∼, ≺, ≈, ≾, ◁_{S}, ◁_{FS}} we write Δ ⊑_{R}^{μ} Θ just when Δ ∈[[φ]] ⇒ Θ ∈[[φ]] for all closed φ ∈ L_{R}^{μ}, and Δ ⊑_{R} Θ just when Δ ∈[[φ]] ⇒ Θ ∈[[φ]] for all φ ∈ L_{R}.

Note that the relations ⊑_{∼}^{μ}, ⊑_{≈}^{μ}, ⊑_{∼} and ⊑_{≈} are symmetric. For this reason we will employ the symbol ≡ instead of ⊑ when referring to them.

We have the following modal characterisation for strong probabilistic bisimilarity, strong probabilistic similarity, weak probabilistic bisimilarity, weak probabilistic similarity, forward similarity, and failure similarity.

Theorem 4 (Modal characterisation). Let s and t be states in a divergence-free pLTS.

1. s ∼ t iff \overline{s} ≡_{∼}^{μ} \overline{t} iff \overline{s} ≡_{∼} \overline{t}.
2. s ≺ t iff \overline{s} ⊑_{≺}^{μ} \overline{t} iff \overline{s} ⊑_{≺} \overline{t}.
3. s ≈ t iff \overline{s} ≡_{≈}^{μ} \overline{t} iff \overline{s} ≡_{≈} \overline{t}.
4. s ≾ t iff \overline{s} ⊑_{≾}^{μ} \overline{t} iff \overline{s} ⊑_{≾} \overline{t}.
5. s ◁_{S} Θ iff \overline{s} ⊑_{◁_{S}}^{μ} Θ iff \overline{s} ⊑_{◁_{S}} Θ.
6. s ◁_{FS} Θ iff \overline{s} ⊑_{◁_{FS}}^{μ} Θ iff \overline{s} ⊑_{◁_{FS}} Θ.

Note that \overline{s} ≡_{∼}^{μ} \overline{t} ⇒ s ∼ t is an immediate consequence of Theorem 2: From s ∼ s we obtain \overline{s} ∈ [[ν_{E}(X_{s})]]. Together with \overline{s} ≡_{∼}^{μ} \overline{t} this yields \overline{t} ∈ [[ν_{E}(X_{s})]], hence s ∼ t.

Proof. We only prove the first statement; the others can be shown analogously. In fact we establish the more general result that

Δ ∼^{†} Θ  ⇔  Δ ≡_{∼}^{μ} Θ  ⇔  Δ ≡_{∼} Θ

from which statement 1 of Theorem 4 follows immediately. The implication Δ ∼^{†} Θ ⇒ Δ ≡_{∼}^{μ} Θ expresses the soundness of the logic L_{∼}^{μ} w.r.t. the relation ∼^{†}, whereas the implication Δ ≡_{∼} Θ ⇒ Δ ∼^{†} Θ expresses the completeness of L_{∼} w.r.t. ∼^{†}. The implication Δ ≡_{∼}^{μ} Θ ⇒ Δ ≡_{∼} Θ is trivial.

(Soundness) An environment ρ : Var → 𝒫(D(S)) is called compatible with ∼^{†} if for all X ∈ Var we have that

Δ ∼^{†} Θ ⇒ (Δ ∈ ρ(X) ⇒ Θ ∈ ρ(X)).

We will show by structural induction on φ that

Δ ∼^{†} Θ ⇒ (Δ ∈ [[φ]]_{ρ} ⇒ Θ ∈ [[φ]]_{ρ})

for any environment ρ that is compatible with ∼^{†}. By restricting attention to closed φ this implies the soundness of L_{∼}^{μ} w.r.t. ∼^{†}. We consider a few interesting cases.

– Let Δ ∼^{†} Θ and Δ ∈ [[⟨a⟩φ]]_{ρ}. Then Δ ⟶^{a} Δ′ and Δ′ ∈ [[φ]]_{ρ} for some Δ′. It follows that there is some Θ′ with Θ ⟶^{a} Θ′ and Δ′ ∼^{†} Θ′. By induction we have Θ′ ∈ [[φ]]_{ρ}, thus Θ ⊧ ⟨a⟩φ.

– Let Δ ∼^{†} Θ and Δ ∈ [[[a]φ]]_{ρ}. Suppose Θ ⟶^{a} Θ′. It can be seen that there is a Δ′ with Δ ⟶^{a} Δ′ and Δ′ ∼^{†} Θ′. As Δ ∈ [[[a]φ]]_{ρ} it must be that Δ′ ∈ [[φ]]_{ρ}, and by induction we have Θ′ ∈ [[φ]]_{ρ}. Thus Θ ∈ [[[a]φ]]_{ρ}.

– Let Δ ∼^{†} Θ and Δ ∈ [[⨁_{i∈I} p_{i} ·φ_{i}]]_{ρ}. So Δ = ∑_{i∈i} p_{i} ·Δ_{i} and for all i ∈ I we have Δ_{i} ∈ [[φ_{i}]]_{ρ}. Since Δ ∼^{†} Θ, by Proposition 2(2) we have Θ = ∑_{i∈I} p_{i}·Θ_{i} and Δ_{i} ∼^{†} Θ_{i}. So by induction we have Θ_{i} ∈[[φ_{i}]]_{ρ} for all i ∈ I. Therefore, Θ ∈ [[⨁_{i∈I} p_{i} · φ_{i}]]_{ρ}. The case Δ ∈ [[⨁_{i∈I} φ_{i}]]_{ρ} goes likewise.

– Let Δ ∼^{†} Θ and Δ ∈ [[↓φ]]_{ρ}. So for all s ∈ ⌈Δ⌉ we have \overline{s} ∈ [[φ]]_{ρ}. From Δ ∼^{†} Θ it follows that for each t ∈⌈Θ⌉ there is an s ∈⌈Δ⌉ with s ∼ t, thus \overline{s} ∼^{†} \overline{t}. So by induction we have \overline{t} ∈[[φ]]_{ρ} for all t ∈⌈Θ⌉. Therefore, Θ ∈ [[↓φ]]_{ρ}.

– Suppose Δ ∼^{†} Θ and Θ ∉ [[μX.φ]]_{ρ}. Then ∃V ⊆ D(S) with Θ ∉ V and [[φ]]_{ρ[X↦V]} ⊆ V. Let V′ := {Δ′ | ∀Θ′.(Δ′ ∼^{†} Θ′ ⇒ Θ′ ∈ V)}. Then Δ ∉ V′. It remains to show that [[φ]]_{ρ[X↦V′]} ⊆ V′, because this implies Δ ∉ [[μX.φ]]_{ρ}, which has to be shown. So let Δ′ ∈ [[φ]]_{ρ[X↦V′]}. Take any Θ′ with Δ′ ∼^{†} Θ′. By construction of V′, the environment ρ[X ↦ V′] is compatible with ∼^{†}. Therefore, the induction hypothesis yields Θ′ ∈ [[φ]]_{ρ[X↦V′]}. We have V′ ⊆ V, and as [[ ]] is monotonic we obtain Θ′ ∈ [[φ]]_{ρ[X↦V′]} ⊆ [[φ]]_{ρ[X↦V]} ⊆ V. It follows that Δ′ ∈ V′.

– Suppose Δ ∼^{†} Θ and Δ ∈ [[νX.φ]]_{ρ}. Then ∃V ⊆ D(S) with Δ ∈ V and [[φ]]_{ρ[X↦V]} ⊇ V. Let V′ := {Θ′ | ∃Δ′ ∈ V. Δ′ ∼^{†} Θ′}. Then Θ ∈ V′. It remains to show that [[φ]]_{ρ[X↦V′]} ⊇ V′, because this implies Θ ∈ [[νX.φ]]_{ρ}, which has to be shown. So let Θ′ ∉ [[φ]]_{ρ[X↦V′]}. Take any Δ′ with Δ′ ∼^{†} Θ′. By construction of V′, the environment ρ[X ↦ V′] is compatible with ∼^{†}. Therefore, the induction hypothesis yields Δ′ ∉ [[φ]]_{ρ[X↦V′]}. We have V′ ⊇ V, and as [[ ]] is monotonic we obtain Δ′ ∉ [[φ]]_{ρ[X↦V′]} ⊇ [[φ]]_{ρ[X↦V]} ⊇ V. It follows that Θ′ ∉ V′.

(Completeness) Let R = \{(s, t) | \overline{s} ≡_{∼} \overline{t}\}. We show that R is a strong probabilistic bisimulation. Suppose s R t and s ⟶^{a} Δ. We have to show that there is some Θ with \overline{t} ⟶^{a} Θ and Δ R^{†} Θ. Consider the set

T := \{Θ | \overline{t} ⟶^{a} Θ ∧ Θ = ∑_{s′∈⌈Δ⌉} Δ(s′) · Θ_{s′} ∧ ∃s′ ∈ ⌈Δ⌉, ∃t′ ∈ ⌈Θ_{s′}⌉ : \overline{s′} ≢_{∼} \overline{t′}\}

For each Θ ∈ T there must be some s′_{Θ} ∈ ⌈Δ⌉ and t′_{Θ} ∈ ⌈Θ_{s′_{Θ}}⌉ and a formula φ_{Θ} with \overline{s′_{Θ}} ⊧ φ_{Θ} but \overline{t′_{Θ}} |̸= φ_{Θ}. So \overline{s′} ⊧ ⋀_{\{Θ∈T |s′_{Θ}=s′\}} φ_{Θ} for each s′ ∈ ⌈Δ⌉, and for

each Θ ∈ T with s′_{Θ} = s′ there is some t′_{Θ} ∈ ⌈Θ_{s′}⌉ with \overline{t′_{Θ}} |̸= ⋀_{\{Θ∈T |s′_{Θ}=s′\}} φ_{Θ}. Let

φ := ⟨a⟩ ⨁_{s′∈⌈Δ⌉} Δ(s′) · ↓ ⋀_{{Θ∈T |s′_{Θ}=s′}} φ_{Θ}.

It is clear that \overline{s} ⊧ φ, hence \overline{t} ⊧ φ by sRt. It follows that there must be a

Θ^{∗} with \overline{t} ⟶^{a} Θ^{∗}, Θ^{∗} = ∑_{s′∈⌈Δ⌉} Δ(s′) · Θ_{s′}^{∗} and for each s′ ∈⌈Δ⌉, t′ ∈⌈Θ_{s′}^{∗}⌉

we have \overline{t′} ⊧ ⋀_{\{Θ∈T |s′_{Θ}=s′\}} φ_{Θ}. This means that Θ^{∗} ∉ T and hence for each s′ ∈⌈Δ⌉, t′ ∈⌈Θ_{s′}^{∗}⌉ we have \overline{s′} ≡_{∼} \overline{t′}, i.e. s′Rt′. Consequently, we obtain Δ R^{†} Θ^{∗}. By symmetry all transitions of t can be matched up by transitions of s. ⊓ ⊔

Modal characterisation of strong and weak probabilistic bisimulation has been studied in [27]. It is also based on a probabilistic extension of the Hennessy-Milner logic. Instead of our modalities ⨁ and ↓ they use a modality [·]_{p}. Intuitively, a distribution Δ satisfies the formula [φ]_{p} when the set of states satisfying φ is measured by Δ with probability at least p. So the formula [φ]_{p} can be expressed by our logics in terms of the probabilistic choice ⨁_{i∈I} p_{i} · φ_{i} by setting I = {1, 2}, p_{1} = p, p_{2} = 1−p, φ_{1} = ↓φ, and φ_{2} = true. Furthermore, instead of our modality ⟨a⟩, they use a modality ·♢a that can be expressed in our logic by ·♢aφ = ⟨a⟩↓φ. We conjecture that our modalities ⟨a⟩ and ⨁ cannot be expressed in terms of the logic of [27], and that a logic of that type is unsuitable for characterising forward simulation or failure simulation.

When restricted to deterministic pLTSs (i.e., for each state and for each action, there exists at most one outgoing transition), probabilistic bisimulations can be characterised by simpler forms of logics, as observed in [20,11,27].

References

1. E. Bandini & R. Segala (2001): Axiomatizations for Probabilistic Bisimulation. In: Proc. ICALP’01, LNCS 2076, Springer, pp. 370–381.

2. I. Christoff (1990): Testing equivalences and fully abstract models for probabilistic processes. In: Proc. CONCUR’90, LNCS 458, Springer, pp. 126–140.

3. R. Cleaveland, S. Purushothaman Iyer & M. Narasimha (2005): Probabilistic temporal logics via the modal mu-calculus. Theoretical Computer Science 342(2-3), pp. 316–350.

4. P.R. D’Argenio, N. Wolovick, P.S. Terraf & P. Celayes (2009): Nondeterministic Labeled Markov Processes: Bisimulations and Logical Characterization. In: Proc. QEST’09, IEEE Computer Society, pp. 11–20.

5. Y. Deng & W. Du (2009): A Local Algorithm for Checking Probabilistic Bisimilarity. In: Proc. FCST’09, IEEE Computer Society, pp. 401–407.

6. Y. Deng & R.J. van Glabbeek. Characterising Probabilistic Processes Logically. Available at http://arxiv.org/abs/1007.5188. Full version of this paper.

7. Y. Deng, R.J. van Glabbeek, M. Hennessy & C.C. Morgan (2008): Characterising Testing Preorders for Finite Probabilistic Processes. Logical Methods in Computer Science 4(4):4.

8. Y. Deng, R.J. van Glabbeek, M. Hennessy & C.C. Morgan (2009): Testing Finitary Probabilistic Processes. In: Proc. CONCUR’09, LNCS, Springer, pp. 274–288.

9. Y. Deng, R.J. van Glabbeek, M. Hennessy, C.C. Morgan & C. Zhang (2007): Remarks on Testing Probabilistic Processes. ENTCS 172, pp. 359–397.

10. Y. Deng & C. Palamidessi (2007): Axiomatizations for probabilistic finite-state behaviors. Theoretical Computer Science 373(1-2), pp. 92–114.

11. J. Desharnais, A. Edalat & P. Panangaden (1998): A logical characterization of bisimulation for labelled Markov processes. In: Proc. LICS’98, IEEE Computer Society, pp. 478–489.

12. A. Giacalone, C.-C. Jou & S.A. Smolka (1990): Algebraic reasoning for probabilistic concurrent systems. In: Proc. IFIP TC 2 Working Conference on Programming Concepts and Methods, pp. 443–458.

13. H. Hansson & B. Jonsson (1990): A Calculus for Communicating Systems with Time and Probabilities. In: Proc. RTSS’90, IEEE Computer Society, pp. 278–287.

14. H. Hansson & B. Jonsson (1994): A Logic for Reasoning about Time and Reliability. Formal Aspects of Computing 6(5), pp. 512–535.

15. M. Hennessy & R. Milner (1985): Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32(1), pp. 137–161.

16. M. Huth & M. Kwiatkowska (1997): Quantitative analysis and model checking. In: Proc. LICS’97, IEEE Computer Society, pp. 111–122.

17. B. Jonsson & K.G. Larsen (1991): Specification and refinement of probabilistic processes. In: Proc. LICS’91, Computer Society Press, pp. 266–277.

18. B. Jonsson & Wang Yi (2002): Testing preorders for probabilistic processes can be characterized by simulations. Theoretical Computer Science 282(1), pp. 33–51.

19. D. Kozen (1983): Results on the propositional mu-calculus. Theoretical Computer Science 27, pp. 333–354.

20. K.G. Larsen & A. Skou (1991): Bisimulation through probabilistic testing. Information and Computation 94(1), pp. 1–28.

21. G. Lowe (1995): Probabilistic and Prioritized Models of Timed CSP. Theoretical Computer Science 138, pp. 315–352.

22. A.K. McIver & C.C. Morgan (1997): An expectation-based model for probabilistic temporal logic. Technical Report PRG-TR-13-97, Oxford University Computing Laboratory.

23. A.K. McIver & C.C. Morgan (2007): Results on the Quantitative Mu-Calculus. ACM Transactions on Computational Logic 8(1).

24. R. Milner (1989): Communication and Concurrency. Prentice Hall.

25. M.W. Mislove, J. Ouaknine & J. Worrell (2004): Axioms for Probability and Nondeterminism. ENTCS 96, pp. 7–28.

26. M. Müller-Olm (1998): Derivation of Characteristic Formulae. ENTCS 18, pp. 159–170.

27. A. Parma & R. Segala (2007): Logical Characterizations of Bisimulations for Discrete Probabilistic Systems. In: Proc. FOSSACS’07, LNCS 4423, Springer, pp. 287–301.

28. M.L. Puterman (1994): Markov Decision Processes. Wiley.

29. Y.S. Ramakrishna & S.A. Smolka (1997): Partial-order reduction in the weak modal mu-calculus. In: A. Mazurkiewicz & J. Winkowski, editors: Proc. CONCUR’97, LNCS 1234, Springer, pp. 5–24.

30. R. Segala (1995): Modeling and Verification of Randomized Distributed Real-Time Systems. Technical Report MIT/LCS/TR-676, PhD thesis, MIT, Dept. of EECS.

31. R. Segala & N.A. Lynch (1994): Probabilistic Simulations for Probabilistic Processes. In: Proc. CONCUR’94, LNCS 836, Springer, pp. 481–496.

32. B. Steffen & A. Ingólfsdóttir (1994): Characteristic Formulae for Processes with Divergence. Information and Computation 110, pp. 149–163.

33. A. Tarski (1955): A lattice-theoretical fixpoint theorem and its application. Pacific Journal of Mathematics 5(2), pp. 285–309.

34. R. Tix, K. Keimel & G.D. Plotkin (2005): Semantic Domains for Combining Probability and Non-Determinism. ENTCS 129, pp. 1–104.

35. Wang Yi & K.G. Larsen (1992): Testing Probabilistic and Nondeterministic Processes. In: Proc. IFIP TC6/WG6.1 PSTV’92, C-8, North-Holland, pp. 47–61.