Testing Finitary Probabilistic Processes

(Extended Abstract)

Yuxin Deng^{1} ^{⋆}, Rob van Glabbeek^{2}^{,}^{4}, Matthew Hennessy^{3} ^{⋆⋆} & Carroll Morgan^{4} ^{⋆⋆⋆}

1 Shanghai Jiao Tong University, China 2 NICTA, Sydney, Australia 3 Trinity College Dublin, Ireland 4 University of New South Wales, Sydney, Australia

Abstract. We provide both modal- and relational characterisations of may- and must-testing preorders for recursive CSP processes with divergence, featuring probabilistic as well as nondeterministic choice. May testing is characterised in terms of simulation, and must testing in terms of failure simulation. To this end we develop weak transitions between probabilistic processes, elaborate their topological properties, and express divergence in terms of partial distributions.

1 Introduction

It has long been a challenge for theoretical computer scientists to provide a firm mathematical foundation for process-description languages that incorporate both nondeterministic and probabilistic behaviour in such a way that processes are semantically distinguished just when they can be told apart by some notion of testing.

In our earlier work [3, 1] a semantic theory was developed for one particular language with these characteristics, a finite process calculus called pCSP: nondeterminism is present in the form of the standard choice operators inherited from CSP [7], that is P ⊓ Q and P □ Q, while probabilistic behaviour is added via a new choice operator P _{p}⊕ Q in which P is chosen with probability p and Q with probability 1−p. The intensional behaviour of a pCSP process is given in terms of a probabilistic labelled transition system [14, 3], or pLTS, a generalisation of labelled transition systems [12]. In a pLTS the result of performing an action in a given state results in a probability distribution over states, rather than a single state; thus the relations s ⟶^{α} t in an LTS are replaced by relations s ⟶^{α} Δ, with Δ a distribution. Closed pCSP expressions P are interpreted as probability distributions ⟦P ⟧ in the associated pLTS. Our semantic theory [3, 1] naturally generalises the two preorders of standard testing theory [5] to pCSP:

– P ⊑_{pmay} Q indicates that Q is at least as good as P from the point of view of possibly passing probabilistic tests; and

– P ⊑_{pmust} Q indicates instead that Q is at least as good as P from the point of view of guaranteeing the passing of probabilistic tests.

⋆ Deng was supported by the National Natural Science Foundation of China (60703033). ⋆⋆ Hennessy gratefully acknowledges the financial support of Science Foundation Ireland. ⋆⋆⋆ Morgan acknowledges the support of ARC Discovery Grant DP0879529.

The most significant result of [1] was an alternative characterisation of these preorders as particular forms of coinductively defined simulation relations, ⊑_{S} and ⊑_{FS}, over the underlying pLTS. We also provided a characterisation in terms of a modal logic.

The object of the current paper is to extend the above results to a version of pCSP with recursive process descriptions: we add a construct rec x. P for recursion, and extend the intensional semantics of [1] in a straightforward manner. We restrict ourselves to finitary pCSP processes, those having finitely many states and displaying finite branching.

Fig. 1. The pLTSs of processes Q_{1} and Q_{2} The simulation relations ⊑_{S} and ⊑_{FS} in [1] were defined in terms of weak transitions ⟹^{τ̂} between distributions, obtained as the transitive closure of a relation ⟶^{τ̂} between distributions that allows one part of a distribution to make a τ-move with the other part remaining in place. This definition is however inadequate for processes that can do an unbounded number of τ-steps. The problem is highlighted by the process Q_{1} = rec x. (τ.x _{\frac{1}{2}} ⊕ a. 0) illustrated in Figure 1(a). Process Q_{1} is indistinguishable, using tests, from the simple process a. 0: we have Q_{1} ≃_{pmay} a. 0 and Q_{1} ≃_{pmust} a. 0. This is because the process Q_{1} will eventually perform the action a with probability 1. However, the action ⟦a. 0 ⟧ ⟶^{a} ⟦ 0 ⟧ can not be simulated by a corresponding move ⟦Q_{1}⟧ ⟹^{τ̂}⟶^{a}. No matter which distribution Δ we obtain from executing a finite sequence of internal moves ⟦Q_{1}⟧ ⟹^{τ̂} Δ, still part of it is unable to subsequently perform the action a.

To address this problem we propose a new relation Δ ⟹ Θ, that indicates that Θ can be derived from Δ by performing an unbounded sequence of internal moves; we call Θ a weak derivative of Δ. For example ⟦a. 0 ⟧ will turn out to be a weak derivative of ⟦Q_{1}⟧, ⟦Q_{1}⟧ ⟹ ⟦a. 0 ⟧, via the infinite sequence of internal moves

⟦Q_{1}⟧ ⟶^{τ} ⟦Q_{1} _{\frac{1}{2}} ⊕ a. 0 ⟧ ⟶^{τ} ⟦Q_{1} _{\frac{1}{2^{2}}} ⊕ a. 0 ⟧ ⟶^{τ} … ⟦Q_{1} _{\frac{1}{2^{n}}} ⊕ a. 0 ⟧ ⟶^{τ} ….

One of our contributions here is the significant use of “sub distributions” that sum to no more than one [8, 11]. For example, the empty subdistribution ε elegantly represents the chaotic behaviour of processes that in CSP and in must-testing semantics is tantamount to divergence, because we have ε ⟶^{α} ε for any action α, and a process like rec x. x that diverges via an infinite τ path gives rise to the weak transition rec x. x ⟹ ε. So the process Q_{2} = Q_{1} _{\frac{1}{2}} ⊕ rec x. x illustrated in Figure 1(b) will enable the weak transition ⟦Q_{2}⟧ ⟹ \frac{1}{2}⟦a. 0 ⟧, where intuitively the latter is a proper subdistribution mapping the state a. 0 to the probability \frac{1}{2}. Our weak transition relation ⟹ can be regarded as an extension of the weak hyper-transition from [10] to partial distributions; the latter, although defined in a very different way, can be represented in terms of ours by requiring weak derivatives to be total distributions.

We end this introduction with a brief glimpse at our proof strategy. In [1] the characterisations for finite pCSP processes were obtained using a probabilistic extension of the Hennessy-Milner logic [12]. Moving to recursive processes, we know that process behaviour can be captured by a finite modal logic only if the underlying LTS is finitely branching, or at least image-finite [12]. Thus to take advantage of a finite probabilistic HML we need a property of pLTSs corresponding to finite branching in LTSs: this is topological compactness, whose relevance we now sketch.

Subdistributions over (derivatives of) finitary pCSP processes inherit the standard (complete) Euclidean metric. One of our key results is that

Theorem 1. For every finitary pCSP process P, the set { Δ | ⟦P ⟧ ⟹ Δ } is convex and compact.

Indeed, using techniques from Markov Decision Theory [13] we can show that the potentially uncountable set { Δ | ⟦P ⟧ ⟹ Δ } is nevertheless the convex closure of a finite set of subdistributions, from which Theorem 1 follows.

This key result allows an inductive characterisation of the simulation preorders ⊑_{S} and ⊑_{FS}, here defined using our novel weak derivation relation ⟹. We first construct a sequence of approximations ⊑_{S}^{k} for k ≥ 0 and, using Theorem 1, we prove

Theorem 2. For every finitary pCSP process P, and for every k ≥ 0, the set { Δ | ⟦P ⟧ ⊑_{S}^{k} Δ } is convex and compact.

This in turn enables us to use the Finite Intersection Property of compact sets to prove

Theorem 3. For finitary pCSP processes we have P ⊑_{S} Q iff P ⊑_{S}^{k} Q for all k ≥ 0.

Our main characterisation results can then be obtained by extending the probabilistic modal logic used in [1], so that for example

– it characterises ⊑_{S}^{k} for every k ≥ 0, and therefore it also characterises ⊑_{S}

– every probabilistic modal formula can be captured by a may-test.

Similar results accrue for must testing and the new failure simulation preorder ⊑_{FS}: details are given in Section 6.

Due to lack of space, we omit proofs, and most examples: they are reported in [2].

2 The Language pCSP

Let Act be a set of visible actions which a process can perform, and let Var be an infinite set of variables. The language pCSP of probabilistic CSP processes is given by the following two-sorted syntax, in which p ∈ [0, 1], a ∈ Act and A ⊆ Act:

\begin{aligned}P & ::= & S | P_{p}⊕ P \\ S & ::= & 0 | x ∈ Var | a.P | P ⊓ P | S □ S | S |_{A} S | rec x. P . \end{aligned}

a.P ⟶^{a} ⟦P⟧  rec x. P ⟶^{τ} ⟦P [x ↦ rec x. P]⟧
P ⊓ Q ⟶^{τ} ⟦P⟧  P ⊓ Q ⟶^{τ} ⟦Q⟧
\frac{s_{1} ⟶^{a} Δ}{s_{1} □ s_{2} ⟶^{a} Δ}  \frac{s_{2} ⟶^{a} Δ}{s_{1} □ s_{2} ⟶^{a} Δ}
\frac{s_{1} ⟶^{τ} Δ}{s_{1} □ s_{2} ⟶^{τ} Δ □ s_{2}}  \frac{s_{2} ⟶^{τ} Δ}{s_{1} □ s_{2} ⟶^{τ} s_{1} □ Δ}
\frac{s_{1} ⟶^{α} Δ α ∉ A}{s_{1} |_{A} s_{2} ⟶^{α} Δ |_{A} s_{2}}  \frac{s_{2} ⟶^{α} Δ α ∉ A}{s_{1} |_{A} s_{2} ⟶^{α} s_{1} |_{A} Δ}

\frac{s_{1} ⟶^{a} Δ_{1}, s_{2} ⟶^{a} Δ_{2} a ∈ A}{s_{1} |_{A} s_{2} ⟶^{τ} Δ_{1} |_{A} Δ_{2}}

Fig. 2. Operational semantics of pCSP

This is essentially the finite language of [1, 3] plus the recursive construct rec x. P in which x is a variable and P a term. The notions of free- and bound variables are standard; by Q[x ↦ P] we indicate substitution of term P for variable x in Q, with renaming if necessary. We write pCSP for the set of closed P -terms defined by this grammar, and sCSP for its state-based subset of closed S-terms.

Following [3, 1], we interpret the language as a probabilistic labelled transition system. A (discrete) probability subdistribution over a set S is a function Δ : S → [0, 1] with ∑_{s ∈ S} Δ(s) ≤ 1; the support of such a Δ is ⌈Δ⌉ := { s ∈ S | Δ(s) > 0 }, and its mass |Δ| is ∑_{s ∈⌈Δ⌉} Δ(s). A subdistribution is a (total, or full) distribution if |Δ| = 1. The point distribution \overline{s} assigns probability 1 to s and 0 to all other elements of S, so that ⌈\overline{s}⌉ = \{s\}. With D_{sub}(S) we denote the set of subdistributions over S, and with D(S) its subset of full distributions.

Let {Δ_{k} | k ∈ K} be a set of subdistributions, possibly infinite. Then ∑_{k∈K} Δ_{k} is the real-valued function in S → ℝ defined by (∑_{k∈K} Δ_{k})(s) := ∑_{k∈K} Δ_{k}(s). This is a partial operation on subdistributions because for some state s the sum of Δ_{k}(s) might exceed 1. If the index set is finite, say {1..n}, we often write Δ_{1} + … + Δ_{n}. For p a real number from [0, 1] we use p·Δ to denote the subdistribution given by (p·Δ)(s) := p·Δ(s). Finally we use ε to denote the everywhere-zero subdistribution that thus has empty support. These operations on subdistributions do not readily adapt themselves to distributions; yet if that ∑_{k∈K} p_{k} = 1 for some collection of p_{k} ≥ 0, and the Δ_{k} are distributions, then so is ∑_{k∈K} p_{k} ·Δ_{k}. In general when 0≤p≤1 we write x_{p}⊕ y for p·x + (1−p)·y where that makes sense, so that for example Δ_{1}_{p}⊕ Δ_{2} is always defined, and is full if Δ_{1} and Δ_{2} are.

The expected value ∑_{s∈S} Δ(s)·f(s) over a distribution Δ of a bounded nonnegative function f to the reals or tuples of them is written Exp_{Δ}(f), and the image of a distribution Δ through a function f is written Img_{f}(Δ) — the latter is the distribution over the range of f given by Img_{f}(Δ)(t) := ∑_{f(s)=t} Δ(s).

Definition 1. A probabilistic labelled transition system (pLTS) is a triple ⟨S, L, →⟩, where

(i) S is a set of states, (ii) L is a set of transition labels, (iii) relation → is a subset of S × L × D(S).

A (non-probabilistic) labelled transition system (LTS) may be viewed as a degenerate pLTS — one in which only point distributions are used. As with LTSs, we write s ⟶^{α} Δ for (s, α, Δ) ∈ →, as well as s ⟶^{α} for ∃Δ : s ⟶^{α} Δ and s→ for ∃α: s ⟶^{α}. A pLTS is finitely branching if the set {Δ | s ⟶^{α} Δ, α ∈ L} is finite for all states s; if moreover S is finite, then the pLTS is finitary. A subdistribution Δ in an arbitrary pLTS is finitary if restricting the state set to the states reachable from Δ yields a finitary sub-pLTS.

The operational semantics of pCSP is defined by a particular pLTS ⟨sCSP, Act_{τ} , →⟩ in which sCSP is the set of states and Act_{τ} := Act∪{τ} is the set of transition labels; we let a range over Act and α over Act_{τ}. We interpret pCSP processes P as distributions ⟦P ⟧ ∈ D(sCSP) via the function ⟦ ⟧ : pCSP → D(sCSP) defined by

⟦s⟧ := \overline{s} for s ∈ sCSP, and ⟦P_{p}⊕ Q⟧ := ⟦P ⟧_{p}⊕ ⟦Q⟧ .

The relations ⟶^{α} are defined in Figure 2 which extends the rules used in [3, 1] for finite processes with a new rule for recursion. External choice and parallel composition use an abbreviation for distributing an operator over a distribution: for example Δ □ s is the distribution given by (Δ □ s)(t) := Δ(s′) if t is s′ □ s and 0 otherwise. We sometimes write τ.P for P ⊓ P, thus giving τ.P ⟶^{τ} ⟦P ⟧.

Note that this pLTS is finitely branching and for each P ∈ pCSP the distribution ⟦P ⟧ has finite support. However, it is possible for there to be infinitely many states reachable from ⟦P ⟧. If only finitely many states are reachable from ⟦P ⟧, then P is called finitary.

3 Testing Probabilistic Processes

We follow the approach of [3, 1] to the testing of probabilistic processes. A test is simply a process from the language pCSP except that it may use extra visible actions ω_{i}∉Act_{τ}, which are assumed to be fresh, for reporting success. Given a set of test actions Ω, we write pCSP^{Ω} for the set of pCSP expressions using actions from Ω ∪ Act_{τ}, and sCSP^{Ω} for the set of state-based pCSP^{Ω} expressions. To apply test T to process P we form the process T |_{Act} P in which all visible actions except the ω_{i} must synchronise, leaving only actions τ and ω_{i}, and as in [3, 1] we extract testing outcomes from them. However, as processes T |_{Act} P are in general not of finite depth, we can no longer do this inductively. Below we outline two alternative methods that for finitary systems will turn out to be equivalent. The first one is slightly easier to explain, whereas the second one extends the work of [15, 14, 4] and is needed in establishing our results.

3.1 Extremal Testing

For the first method we assume that tests may use only a single success action ω. We view the unit interval [0, 1] ordered in the standard manner as a complete lattice; this induces a complete lattice on the set of functions sCSP^{Ω} → [0, 1]. Now consider the function R_{min} : (sCSP^{Ω}→[0, 1]) → (sCSP^{Ω}→[0, 1]) defined by

R_{min}(f)(s) := \begin{cases}1 & if s ⟶^{ω} \\ 0 & if s ↛ \\ min\{ Exp_{Δ}(f) | s ⟶^{α} Δ \} & otherwise. \end{cases}

In a similar fashion we define the function R_{max} which uses max in place of min. Both these functions are monotonic, and therefore have least fixed points which we call 𝕍_{min}, 𝕍_{max} respectively.

Now for a test T and a process P we have two ways of defining the outcome of the application of T to P:

A_{min}^{e}(T, P) := Exp_{⟦T |_{Act}P⟧}(𝕍_{min})
A_{max}^{e}(T, P) := Exp_{⟦T |_{Act}P⟧}(𝕍_{max}) .

Here A_{min}^{e}(T, P) returns a single probability p, estimating the minimum probability of success; it is a pessimistic estimate. On the other hand A_{max}^{e}(T, P) is optimistic, in that it gives the maximum probability of success.

Definition 2. The may- and must preorders are given by

– P ⊑_{pmay}^{e} Q if for every test T we have A_{max}^{e}(T, P) ≤ A_{max}^{e}(T, Q)

– P ⊑_{pmust}^{e} Q if for every test T we have A_{min}^{e}(T, P) ≤ A_{min}^{e}(T, Q).

3.2 Resolution-based Testing

In the second method we use Ω-tests for any given collection Ω of success actions disjoint from Act_{τ}; here ω will be a variable ranging over the individual success actions of Ω. We calculate the result of applying test T to process P in terms of the resolutions of the combined process T |_{Act} P, where intuitively a resolution represents a run of a process and, as such, gives exactly one probability for each success action. So in general the application of T to P will yield a set of vectors of probabilities.

We define the resolutions of a process T |_{Act} P in terms of the distribution ⟦T |_{Act} P ⟧ in the pLTS ⟨sCSP^{Ω} |_{Act} sCSP, Ω_{τ} , →⟩ obtained by restricting attention to states of the form t |_{Act} s with t ∈ sCSP^{Ω} and s ∈ sCSP. Note that all transitions in this pLTS have labels τ or ω ∈ Ω. Following [5, 15, 3, 1], and unlike [14, 4], this paper employs state-based testing [4, 1], meaning that transitions s ⟶^{ω} Δ are merely expedients to mark the state s as an ω-success state — the target distribution Δ is wholly ignored. Hence the pLTS can also be regarded as having just τ-labels and moreover state markers ω ∈ Ω. Intuitively, a resolution of a distribution in such a pLTS is obtained by pruning away multiple τ-transitions from a state until only a single choice remains, possibly introducing some linear combinations in the process.

Definition 3. A pLTS ⟨R, L, →⟩ is deterministic if for every r ∈ R and every α ∈ L there is at most one Θ ∈ D_{sub}(R) such that r ⟶^{α} Θ.

A resolution of a subdistribution Δ ∈ D_{sub}(S) in a pLTS ⟨S, Ω_{τ} , →⟩ is a triple ⟨R, Θ, →′⟩ where ⟨R, Ω_{τ} , →′⟩ is a deterministic pLTS and Θ ∈ D_{sub}(R), such that there exists a resolving function f ∈ R → S satisfying 1. Img_{f}(Θ) = Δ

2. if r ⟶^{α}′ Θ′ for α ∈ Ω_{τ} then f(r) ⟶^{α} Img_{f}(Θ′)

3. if f(r) ⟶^{α} for α ∈ Ω_{τ} then r ⟶^{α}′ .

By analogy with the functions R_{min} and R_{max} of Section 3.1, we define the function R : (R→[0, 1]^{Ω}) → (R→[0, 1]^{Ω}) for a deterministic pLTS ⟨R, Ω_{τ} , →⟩ as

R(f)(r)(ω) := \begin{cases}1 & if r ⟶^{ω} \\ 0 & if r −̸→^{ω} and r −̸→^{τ} \\ Exp_{Δ}(f)(ω) & if r −̸→^{ω} and r ⟶^{τ} Δ. \end{cases}

Once more this function has a least fixed point, which we denote by 𝕍_{⟨R,Ω_{τ} ,→⟩}. Now let A^{Ω}(T, P) denote the set of vectors

{ Exp_{Θ}(𝕍_{⟨R,Ω_{τ} ,→⟩}) | ⟨R, Θ, →⟩ is a resolution of ⟦T |_{Act} P ⟧ } .

We compare two vectors of probabilities component-wise, and two sets of vectors of probabilities via the Hoare- and Smyth preorders:

X ≤_{Ho} Y iff ∀x ∈ X : ∃y ∈ Y : x ≤ y
X ≤_{Sm} Y iff ∀y ∈ Y : ∃x ∈ X : x ≤ y .

Definition 4. Given two pCSP processes P and Q,

– P ⊑_{pmay}^{Ω} Q if for every Ω-test T, we have A^{Ω}(T, P) ≤_{Ho} A^{Ω}(T, Q)

– P ⊑_{pmust}^{Ω} Q if for every Ω-test T, we have A^{Ω}(T, P) ≤_{Sm} A^{Ω}(T, Q). These preorders are abbreviated to P ⊑_{pmay} Q and P ⊑_{pmust} Q when |Ω|= 1.

3.3 Equivalence of Testing Methods

In this section we compare the two approaches of testing introduced in the previous two subsections. First of all, we recall the result from [4] which says that when testing finitary processes it suffices to use a single success action rather than multiple ones.^{1}

Theorem 4. For finitary processes:

P ⊑_{pmay}^{Ω} Q iff P ⊑_{pmay} Q and P ⊑_{pmust}^{Ω} Q iff P ⊑_{pmust} Q.

The following theorem states that, for finitary processes, extremal testing yields the same preorders as resolution-based testing with a single success action.

Theorem 5. For finitary processes

P ⊑_{pmay}^{e} Q iff P ⊑_{pmay} Q and P ⊑_{pmust}^{e} Q iff P ⊑_{pmust} Q.

Neither result in Theorem 5 is true in the general (non-finitary) case, as counterexamples in [2, App. A] demonstrate. Although Theorem 4 suggests that we could have avoided multiple success actions in the resolution-based definition of testing, our completeness proof (Theorem 15) makes essential use of a countable set of them.

1 The result in [4] is stated for action-based testing, meaning that it is the actual execution of a success action rather than reaching a success state that constitutes success, but, as mentioned in the conclusion of [4], it also holds in our current state-based setting.

4 A Novel Approach to Weak Derivations

In this section we develop a new definition of what it means for a recursive process to evolve by silent activity into another process; it allows the simulation and failuresimulation preorders of [1] to be adapted to characterise the testing preorders for at least finitary probabilistic processes. The key technical generalisation is the subdistributions that enable us to express divergence very conveniently.^{2}

In a pLTS actions are only performed by states, in that actions are given by relations from states to distributions. But pCSP processes in general correspond to distributions over states, so in order to define what it means for a process to perform an action we need to lift these relations so that they also apply to (sub)distributions.

Definition 5. Let (S, L, →) be a pLTS and R ⊆ S × D_{sub}(S) be a relation from states to subdistributions. Then \overline{R} ⊆ D_{sub}(S) × D_{sub}(S) is the smallest relation that satisfies (1) s R Θ implies \overline{s} \overline{R} Θ, and

(2) (Linearity) Δ_{i} \overline{R} Θ_{i} for i ∈ I implies (∑_{i∈I} p_{i} ·Δ_{i}) \overline{R} (∑_{i∈I} p_{i} ·Θ_{i}) for any p_{i} ∈ [0, 1] with ∑_{i∈I} p_{i} ≤ 1.

This applies when the relation is ⟶^{α} for α ∈ Act_{τ}, where we also write ⟶^{α} for \overline{⟶^{α}}. Thus as source of a relation ⟶^{α} we now also allow distributions, and even subdistributions. A subtlety of this approach is that for any action α, we have ε ⟶^{α} ε simply by taking I = ∅ or ∑_{i∈I} p_{i} = 0 in Definition 5. That will turn out to make ε especially useful for modelling the “chaotic” aspects of divergence, in particular that in the must-case a divergent process can mimic any other.

We now formally define the notation of weak derivatives.

Definition 6. Suppose we have subdistributions Δ, Δ\overrightarrow{k}, Δ_{k}^{×}, for k ≥ 0, with the following properties:

Δ = Δ\overrightarrow{0} + Δ_{0}^{×}
Δ\overrightarrow{0} ⟶^{τ} Δ\overrightarrow{1} + Δ_{1}^{×}
⋮
Δ\overrightarrow{k} ⟶^{τ} Δ\overrightarrow{k+1} + Δ_{k+1}^{×} .
⋮

Then we call Δ′ := ∑_{k=0}^{∞} Δ_{k}^{×} a weak derivative of Δ, and write Δ ⟹ Δ′ to mean that Δ can make a weak τ move to its derivative Δ′.

It is easy to check that ∑_{k=0}^{∞} Δ_{k}^{×} is indeed a subdistribution, whereas in general it is not a full distribution: for instance we have ⟦rec x. x⟧ ⟹ ε. By setting appropriate Δ_{k}^{×}’s to ε we see that Δ(⟶^{τ})^{∗}Φ, where ^{∗} denotes reflexive and transitive closure, implies Δ ⟹ Φ. It is also easy to check that on recursion-free pCSP the relation ⟹ agrees with the one defined in [3, 1] by means of transitive closure. Moreover the standard notion of divergence, the ability of a subdistribution Δ to perform an infinite sequence of τ transitions, is neatly captured by the relation Δ ⟹ ε.

2 Subdistributions’ nice properties with respect to divergence are due to their being equivalent to the discrete probabilistic powerdomain over a flat domain [8].

Example 1. Consider the (infinite) collection of states s_{k} and probabilities p_{k} for k ≥ 2 such that

s_{k} ⟶^{τ} ⟦a. 0 ⟧_{p_{k}}⊕ \overline{s_{k+1}} ,

where we choose p_{k} so that starting from any s_{k} the probability of eventually taking a left-hand branch, and so reaching ⟦a. 0 ⟧ ultimately, is just 1/k in total. Thus p_{k} must satisfy 1/k = p_{k} +(1−p_{k})/(k+1), whence by arithmetic we have that p_{k} := 1/k^{2} will do. Therefore in particular \overline{s_{2}} ⟹ \frac{1}{2}⟦a. 0 ⟧, with the remaining \frac{1}{2} lost in divergence.

Definition 7. Let Δ and its variants be subdistributions in a pLTS ⟨S, Act_{τ} , →⟩.

– For a ∈ Act write Δ ⟹^{a} Δ′ whenever Δ ⟹ Δ^{pre} ⟶^{a} Δ^{post} ⟹ Δ′. Extend this to Act_{τ} by allowing as a special case that ⟹^{τ} is simply ⟹, i.e. including identity (rather than requiring at least one ⟶^{τ}).

– For A ⊆ Act and s ∈ S write s −̸→^{A} if s −̸→^{α} for every α ∈ A ∪ {τ}; write Δ −̸→^{A} if

s −̸→^{A} for every s ∈⌈Δ⌉.

– More generally write Δ ⟹−̸→^{A} if Δ ⟹ Δ^{pre} for some Δ^{pre} such that Δ^{pre} −̸→^{A}.

For example, in Figure 1 we have ⟦Q_{1}⟧ ⟹^{a} ⟦ 0 ⟧, because ⟦Q_{1}⟧ ⟹ ⟦a. 0 ⟧ ⟶^{a} ⟦ 0 ⟧.

5 Some properties of weak derivations in finitary pLTSs

In this section we expose some less obvious properties of weak derivations from states in finitary pLTSs, relating to their behaviour at infinity; they underpin many results in the next section. One important property is that the set of weak derivations from a single starting point is compact in the sense (from analysis) of being bounded and containing all its limit points, where, in turn, limits depend on a Euclidean-style metric defining the distance between two distributions in a straightforward way. The other property is “distillation of divergence”, allowing us to find in any weak derivation that partially diverges (by no matter how small an amount) a point at which the divergence is “distilled” into a state which wholly diverges.

Both properties depend on our working within finitary pLTSs — that is, ones in which the state space is finite and the (unlifted) transition relation is finite-branching.

5.1 Finite generability and closure

In a finitary pLTS, by definition the sets {Δ | s ⟶^{α} Δ} are finite, for every s and α. This of course is no longer true for the lifted relations ⟶^{α} over subdistributions; nevertheless, the sets \{Δ | \overline{s} ⟶^{α} Δ\} and their weak counterparts \{Δ | \overline{s} ⟹^{α} Δ\} can be finitely represented. Below, we focus on the set \{Δ | \overline{s} ⟹ Δ\}.

Definition 8. A static derivative policy (SDP) for a pLTS ⟨S, Act_{τ} , →⟩ is a partial function pp : S ⇀ D(S) such that if pp is defined at s then s ⟶^{τ} pp(s).

Intuitively a policy pp decides for each state, once and for all, which of the available τchoices to take, if any: since it either chooses a specific transition, or inaction (by being undefined), it does not interpolate via a convex combination of two different transitions; and since it is a function of the state, it makes the same choice on every visit.

The great importance for us of SDP’s is that they give a particularly simple characterisation of weak derivatives, provided the state-space is finite and the pLTS is finitely branching. This is essentially a result of Markov Decision Processes [13], which we translate into our context. We first introduce a notion of SDP-derivatives by adapting Definition 6.

Definition 9 (SDP-derivatives). Let pp be a SDP. We write Δ ⟹_{pp} Δ′ if Δ ⟹ Δ′ and the following holds (using the notation of Def. 6 and writing Δ_{k} for Δ\overrightarrow{k} + Δ_{k}^{×}):

Δ_{k}^{×}(s) = \{ \begin{matrix}0 & if pp defined at s \\ Δ_{k}(s) & otherwise \end{matrix}
Δ_{k+1} = ∑{Δ_{k}(s)· pp(s) | s ∈ ⌈Δ_{k}⌉ and pp defined at s}.

Intuitively, Δ ⟹_{pp} Δ′ means that Δ′ is the single derivative of Δ that results from using policy pp to construct the weak transition Δ ⟹ Δ′. Note that, for a given SDP pp, the relation ⟹_{pp} is actually a function; moreover in a finitary pLTS the set of all possible SDPs is finite, due to the constraints of Definition 8.

Theorem 6 (Finite generability). Let s be a state in a finitary pLTS ⟨S, Act_{τ} , →⟩. Then s ⟹ Δ for some Δ ∈ D_{sub}(S) iff there is a finite index set I, probabilities p_{i} summing to 1 and static derivative policies pp_{i} with s ⟹_{pp_{i}} Δ_{i} for each i, such that Δ = ∑_{i∈I} p_{i} ·Δ_{i}.

Since the convex closure of a finite set of points is always compact, we obtain

Corollary 1. For any state s in a finitary pLTS the set {Δ | s ⟹ Δ} is convex and compact.

A similar result is obtained by Desharnais, Gupta, Jagadeesan & Panagaden [6].

Although the pLTS ⟨sCSP, Act_{τ} , →⟩ is not finitary, the interpretation ⟦P ⟧ ∈ D(sCSP) of a finitary pCSP process P can also be understood to be a distribution in a finitary pLTS, namely the restriction of ⟨sCSP, Act_{τ} , →⟩ to the states reachable from ⟦P ⟧. Using this, Corollary 1 leads to the essential Theorem 1, referred to in the introduction.

5.2 Distillation of divergence

Although it is possible to have processes that diverge with some probability strictly between zero and one, in a finitary pLTS we can distill divergence in the sense that for many purposes we can limit our analyses to processes that either wholly diverge (can do so with probability one) or wholly converge (can diverge only with probability zero). This property is based on the zero-one law for finite-state probabilistic systems, relevant aspects of which we present in this sub-section.

We first note that static derivative policies obey the following zero-one law.

Theorem 7 (Zero-one law). If for a static derivative policy pp over a finite-state pLTS there is for some s a derivation s ⟹_{pp} Δ with |Δ| < 1 then in fact for some (possibly different) state s_{ε} we have s_{ε} ⟹_{pp} ε.

Based on Theorems 6 and 7, the following property of weak derivations can now be established.

Theorem 8 (Distillation of divergence). For any s, Δ in a finitary pLTS with s ⟹ Δ there is a probability p and full distributions Δ_{1}, Δ_{ε} such that s ⟹ (Δ_{1} _{p}⊕ Δ_{ε}) and Δ = p·Δ_{1} and Δ_{ε} ⟹ ε.

6 Failure Simulation is Sound and Complete for Must Testing

In this section we define the failure-simulation preorder and show that it is sound and complete for the must-testing preorder. The following presentation is an enhancement of our earlier definition in [1].

Definition 10 (Failure-Simulation Preorder). Define ⊒_{FS} to be the largest relation in D_{sub}(S) × D_{sub}(S) such that if Δ ⊒_{FS} Θ then

1. whenever Δ ⟹^{α} (∑_{i} p_{i}Δ′_{i}), for α ∈ Act_{τ} and certain p_{i} with (∑_{i} p_{i}) ≤ 1, then there are Θ′_{i} ∈ D_{sub}(S) with Θ ⟹^{α} (∑_{i} p_{i}Θ′_{i}) and Δ′_{i} ⊒_{FS} Θ′_{i} for each i

2. and whenever Δ ⟹−̸→^{A} then also Θ ⟹−̸→^{A}. Naturally Θ ⊑_{FS} Δ just means Δ ⊒_{FS} Θ. For pCSP processes P and Q and any preorder ⊑ ⊆ D_{sub}(sCSP) × D_{sub}(sCSP) we write P ⊑ Q for ⟦P ⟧ ⊑ ⟦Q⟧.

Although the regularity of Definition 10 is appealing — for example it is trivial to see that ⊑_{FS} is reflexive and transitive, as it should be — in practice, for specific processes, it is easier to work with a characterisation of the failure-simulation preorder in terms of a relation between states and subdistributions.

Definition 11 (Failure Similarity). Let ⊲_{FS} be the largest relation in S × D_{sub}(S) such that if s ⊲_{FS} Θ then

1. whenever \overline{s} ⟹ ε then also Θ ⟹ ε,

2. whenever s ⟶^{α} Δ′, for α ∈ Act_{τ}, then there is a Θ′ with Θ ⟹^{α} Θ′ and Δ′ \overline{⊲_{FS}} Θ′ 3. and whenever s −̸→^{A} then Θ ⟹−̸→^{A}.

As an example, in Figure 1 it is straightforward to exhibit failure simulations to prove both ⟦Q_{1}⟧ \overline{⊲_{FS}} ⟦a. 0 ⟧ and the converse ⟦a. 0 ⟧ \overline{⊲_{FS}} ⟦Q_{1}⟧, the essential ingredient being the weak move ⟦Q_{1}⟧ ⟹^{a} ⟦ 0 ⟧. Likewise, we have a. 0 ⊲_{FS} ⟦Q_{1} _{\frac{1}{2}} ⊕ rec x. x⟧, the additional ingredient being 0 ⊲_{FS} ε.

The next result shows how the failure-simulation preorder can alternatively be defined in terms of failure similarity. This is actually how we defined it in [1].

Theorem 9. For finitary Δ, Θ ∈ D_{sub}(S) we have Δ ⊒_{FS} Θ just when there is a Θ^{♮} with Θ ⟹ Θ^{♮} and Δ \overline{⊲_{FS}} Θ^{♮}.

The proof of this theorem depends crucially on Theorems 1 and 8. The restriction to finitary subdistributions is essential, as in [2, App. A] we provide a counterexample to the general case. It is in terms of this characterisation that we establish soundness and completeness of the failure-simulation preorder with respect to the must-testing preorder; consequently we have these results for finitary processes only.

Theorem 10 (Precongruence). If P_{1}, P_{2}, Q_{1} and Q_{2} are finitary pCSP processes with P_{1} ⊒_{FS} Q_{1} and P_{2} ⊒_{FS} Q_{2} then we have α.P_{1} ⊒_{FS} α.Q_{1} for any α ∈ Act_{τ}, as well as P_{1} ⊙ P_{2} ⊒_{FS} Q_{1} ⊙ Q_{2} for ⊙ any of the operators ⊓, □, _{p}⊕ and |_{A}.

The proof of this precongruence property involves a significant complication: in order to relate two processes we have to demonstrate that if the first diverges then so does the second. This affects particularly the proof that ⊒_{FS} is preserved by the parallel operator |_{A}. The approach we use involves first characterising divergence coinductively and then applying a novel coinductive proof technique.

Theorem 11 (Soundness and Completeness). For finitary pCSP processes P and Q we have P ⊑_{FS} Q iff P ⊑_{pmust} Q.

Soundness, that ⊑_{FS} ⊆ ⊑_{pmust}, is a relatively easy consequence of ⊑_{FS} being a precongruence (Theorem 10). The completeness proof (that ⊑_{pmust} ⊆ ⊑_{FS}) is much more complicated and proceeds in three steps, which we detail below. First we provide a characterisation of the preorder relation ⊑_{FS} by finite approximations. Secondly, using this, we develop a modal logic which can be used to characterise the failure-simulation preorder on finitary processes. Finally, we adapt the results of [1] to show that the modal formulae can in turn be characterised by tests. From this, completeness follows.

6.1 Inductive Characterisation

The relation ⊲_{FS} of Definition 11 is given coinductively: it is the largest fixpoint of an equation R= F(R). An alternative approach is to use that F(−) to define ⊲_{FS} as a limit of approximants:

Definition 12. For every k ≥ 0 we define the relations ⊲k_{FS} ⊆ S × D_{sub}(S) as follows:

(i) ⊲0_{FS} := S × D_{sub}(S)

(ii) ⊲k+1_{FS} := F(⊲k_{FS})

Finally let ⊲∞_{FS} := ⋂_{k=0}^{∞} ⊲k_{FS}. Furthermore, for every k ≥ 0 let Δ ⊒_{FS}^{k} Θ if there exists a Θ ⟹ Θ^{♮} with Δ \overline{⊲k_{FS}} Θ^{♮}, and let ⊒_{FS}^{∞} denote ⋂_{k=0}^{∞} ⊒_{FS}^{k}.

Theorem 12. For finitary pCSP processes P and Q we have P ⊒_{FS}^{∞} Q iff P ⊒_{FS} Q.

To show this theorem, we need to use two key results, Propositions 1 and 2 below. We say a relation R ⊆ S × D(S) is convex (resp. compact) whenever the set {Δ | s R Δ} is convex (resp. compact) for every s ∈ S.

Proposition 1. In a finitary pLTS, the relation ⊲k_{FS} is convex and compact, for every k ≥ 0.

The proof of this property heavily relies on Corollary 1.

Proposition 2. Suppose R^{k} ⊆ S × D_{sub}(S) is a sequence of convex and compact relations such that R^{k+1} ⊆ R^{k}. Then (⋂_{k=0}^{∞} \overline{R^{k}}) ⊆ \overline{(⋂_{k=0}^{∞} R^{k})}.

This proposition is proved using the Finite Intersection Property of compact sets [9].

6.2 A Modal Logic

Let F be the set of modal formulae defined inductively as follows:

– div, ⊤ ∈ F

– ref(A) ∈ F when A ⊆ Act,

– ⟨a⟩φ ∈ F when φ ∈ F and a ∈ Act,

– φ_{1} ∧ φ_{2} ∈ F when φ_{1}, φ_{2} ∈ F,

– φ_{1}_{p}⊕ φ_{2} ∈ F when φ_{1}, φ_{2} ∈ F and p ∈ [0, 1].

This generalises the modal language used in [1] by the addition of the new constant div, representing the ability of a process to diverge.

Relative to a given pLTS ⟨S, Act_{τ} , →⟩ the satisfaction relation ⊧ ⊆ D_{sub}(S) × F is given by:

– Δ ⊧ ⊤ for any Δ ∈ D_{sub}(S),

– Δ ⊧ div iff Δ ⟹ ε,

– Δ ⊧ ref(A) iff Δ ⟹−̸→^{A},

– Δ ⊧ ⟨a⟩φ iff there is a Δ′ with Δ ⟹^{a} Δ′ and Δ′ ⊧ φ,

– Δ ⊧ φ_{1} ∧ φ_{2} iff Δ ⊧ φ_{1} and Δ ⊧ φ_{2},

– Δ ⊧ φ_{1}_{p}⊕ φ_{2} iff there are Δ_{1}, Δ_{2} ∈ D_{sub}(S) with Δ_{1} ⊧ φ_{1} and Δ_{2} ⊧ φ_{2}, such that Δ ⟹ Δ_{1}_{p}⊕ Δ_{2}.

We write Δ ⊒^{F} Θ when Δ ⊧ φ implies Θ ⊧ φ for all φ ∈ F, and can verify that ⊒_{FS} is sound for ⊒^{F}. In establishing the converse, we mimic the development in Section 7 of [1] by designing characteristic formulae which capture the behaviour of states in a pLTS. But here the behaviour is not characterised relative to ⊲_{FS}, but rather to the sequence of approximating relations ⊲k_{FS}.

Definition 13. In a finitary pLTS ⟨S, Act_{τ} , →⟩, the k^{th} characteristic formulae φ_{s}^{k}, φ_{Δ}^{k} of states s ∈ S and subdistributions Δ ∈ D_{sub}(S) are defined inductively as follows:

– φ_{s}^{0} = ⊤ and φ_{Δ}^{0} = ⊤,

– φ_{s}^{k+1} = div, provided \overline{s} ⟹ ε,

– φ_{s}^{k+1} = ref(A) ∧ ⋀_{s⟶^{a}Δ}⟨a⟩φ_{Δ}^{k} where A = {a ∈ Act | s −̸→^{a}}, provided s −̸→^{τ},

– φ_{s}^{k+1} = ⋀_{s⟶^{a}Δ}⟨a⟩φ_{Δ}^{k} ∧ ⋀_{s⟶^{τ}Δ} φ_{Δ}^{k} otherwise,

– and φ_{Δ}^{k+1} = (⨁_{s∈⌈Δ⌉} \frac{Δ(s)}{⌈Δ⌉} ·φ_{s}^{k+1}) _{⌈Δ⌉}⊕ (div) .

The next result relates the k^{th} characteristic formulae to the k^{th} failure similarity.

Proposition 3. For k ≥ 0 we have

(i) Θ ⊧ φ_{s}^{k} implies s ⊲k_{FS} Θ, (ii) Θ ⊧ φ_{Δ}^{k} implies Θ ⊒_{FS}^{k} Δ.

Using Proposition 3 we obtain a logical characterisation of ⊒_{FS}^{∞} (and hence of ⊒_{FS}):

Theorem 13. For finitary pCSP processes P and Q we have P ⊒^{F} Q iff P ⊒_{FS}^{∞} Q.

6.3 Characteristic Tests for Formulae

The import of Theorems 12 and 13 is that we can obtain completeness of the failuresimulation preorder with respect to the must-testing preorder by designing for each formula φ a test which in some sense characterises the property that a process satisfies φ. This was achieved for the pLTS generated by the recursion-free fragment of pCSP in Section 8 of [1]. Here we have generalised this technique to the pLTS generated by the set of finitary pCSP terms. The crucial property is stated as follows.

Theorem 14. For every formula φ ∈ F there exists a pair (T_{φ}, v_{φ}) with T_{φ} an Ω-test and v_{φ} ∈ [0, 1]^{Ω} such that Δ ⊧ φ if and only if ∃o ∈ A^{Ω}(T_{φ}, Δ) : o ≤ v_{φ}. Test T_{φ} is called a characteristic test of φ and v_{φ} is its target value.

This property can be shown by exploiting several characteristics of the testing function A^{Ω}(−, −); unlike in [1] these cannot be obtained inductively. The most complicated one is the following.

Proposition 4. If o ∈ A^{Ω}(T_{1} ⊓ T_{2}, Δ) then there are a q ∈ [0, 1] and Δ_{1}, Δ_{2} ∈ D_{sub}(sCSP) such that Δ ⟹ q·Δ_{1} + (1−q)·Δ_{2} and o = q·o_{1} + (1−q)·o_{2} for certain o_{i} ∈ A^{Ω}(T_{i}, Δ_{i}).

From Theorem 14 we obtain that the must-testing preorder is at least as discriminating as the logical preorder:

Theorem 15. Let P and Q be pCSP processes. If P ⊒_{pmust}^{Ω} Q then P ⊒^{F} Q.

The completeness result in Theorem 11 follows by combining Theorems 15, 13 and 12.

7 Simulation is Sound and Complete for May Testing

We define a simulation preorder that can be shown sound and complete for may testing following the same strategy as for failure simulation and must testing, except that we restrict our treatment to full distributions, a simpler domain. This is possible because in may testing an infinite τ-path is not treated specially — it engages in no visible actions; in must testing, infinite τ-paths potentially can do anything (chaos).

Definition 14 (Simulation Preorder). Let ⊑_{S} be the largest relation in D(S) × D(S) such that if Δ ⊑_{S} Θ then

whenever Δ ⟹^{α} (∑_{i} p_{i}Δ′_{i}), for α ∈ Act_{τ} and certain p_{i} with (∑_{i} p_{i}) ≤ 1,

then there are Θ′_{i} ∈ D(S) with Θ ⟹^{α} (∑_{i} p_{i}Θ′_{i}) and Δ′_{i} ⊑_{S} Θ′_{i} for each i.

The technical development from this point on is similar to that given in Section 6. For the modal logic, we use the set of formulae obtained from F by skipping the div and ref(A) clauses. However the satisfaction relation used for this sub-logic is radically different from that given in Section 6.2, because here the interpretation is relative to full distributions. Nevertheless we still obtain the counterparts of Theorems 12, 13 and 15.

Theorem 16 (Soundness and Completeness). For finitary pCSP processes P and Q we have P ⊑_{pmay} Q if and only if P ⊑_{S} Q.

8 Conclusion and Related Work

In this paper we continued our previous work [3, 4, 1] in our quest for a testing theory for processes which exhibit both nondeterministic and probabilistic behaviour. We have generalised our results in [1] of characterising the may preorder as a simulation relation and the must preorder as a failure-simulation relation, from finite processes to finitary processes. To do this it was necessary to investigate fundamental structural properties of derivation sets (finite generability) and similarities (infinite approximations), which are of independent interest. The use of Markov Decision Processes and Zero-One laws was essential in obtaining our results.

Segala [14] defined two preorders called trace distribution precongruence (⊑_{TD}) and failure distribution precongruence (⊑_{FD}). He proved that the former coincides with an action-based version of ⊑_{pmay}^{Ω} and that for “probabilistically convergent” systems the latter coincides with an action-based version of ⊑_{pmust}^{Ω}. The condition of probabilistic convergence amounts in our framework to the requirement that for Δ ∈ D(S) and Δ ⟹ Δ′ we have |Δ′| = 1. In [10] it has been shown that ⊑_{TD} coincides with a notion of simulation akin to ⊑_{S}. Other probabilistic extensions of simulation occurring in the literature are reviewed in [3, 1].

References

1. 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).

2. Y. Deng, R.J. van Glabbeek, M. Hennessy & C.C. Morgan (2009): Testing finitary probabilistic processes. Full version of this extended abstract. Available at

http://www.cse.unsw.edu.au/^{∼}rvg/pub/finitary.pdf

3. Y. Deng, R.J. van Glabbeek, M. Hennessy, C.C. Morgan & C. Zhang (2007): Remarks on testing probabilistic processes. ENTCS 172, pp. 359–397.

4. Y. Deng, R.J. van Glabbeek, C.C. Morgan & C. Zhang (2007): Scalar outcomes suffice for finitary probabilistic testing. In Proc. ESOP’07, LNCS 4421, Springer, pp. 363–378.

5. R. De Nicola & M. Hennessy (1984): Testing equivalences for processes. Theoretical Computer Science 34, pp. 83–133.

6. J. Desharnais, V. Gupta, R. Jagadeesan & P. Panagaden (2002): Weak bisimulation is sound and complete for PCTL. In Proc. CONCUR’02, LNCS 2421, Springer, pp. 355-370.

7. C.A.R. Hoare (1985): Communicating Sequential Processes. Prentice-Hall.

8. C. Jones (1990) Probabilistic Non-determinism. Ph.D. Thesis, University of Edinburgh.

9. S. Lipschutz (1965): Schaum’s outline of theory and problems of general topology. McGraw-Hill.

10. N. Lynch, R. Segala & F.W. Vaandrager (2007): Observing branching structure through probabilistic contexts. SIAM Journal on Computing 37(4), pp. 977–1013.

11. A.K. McIver & C.C. Morgan (2005): Abstraction, Refinement and Proof for Probabilistic Systems. Springer.

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

13. M. Puterman (1994): Markov Decision Processes. Wiley.

14. R. Segala (1996): Testing probabilistic automata. In Proc. CONCUR’96, LNCS 1119, Springer, pp. 299–314.

15. Wang Yi & K.G. Larsen (1992): Testing probabilistic and nondeterministic processes. In Proc. PSTV’92, IFIP Transactions C-8, North-Holland, pp. 47–61.