Fixed-point Characterization of Compositionality Properties
of Probabilistic Processes Combinators
Daniel Gebler
Department of Computer Science, VU University Amsterdam,
De Boelelaan 1081a, NL-1081 HV Amsterdam, The Netherlands
e.d.gebler@vu.nl

Simone Tini
Department of Scienza e Alta Tecnologia,
University of Insubria, Via Valleggio 11, I-22100, Como, Italy
simone.tini@uninsubria.it

Bisimulation metric is a robust behavioural semantics for probabilistic processes. Given any SOS
specification of probabilistic processes, we provide a method to compute for each operator of the
language its respective metric compositionality property. The compositionality property of an operator is defined as its modulus of continuity which gives the relative increase of the distance between
processes when they are combined by that operator. The compositionality property of an operator
is computed by recursively counting how many times the combined processes are copied along their
evolution. The compositionality properties allow to derive an upper bound on the distance between
processes by purely inspecting the operators used to specify those processes.
Keywords: SOS, probabilistic transition systems, bisimulation metric, compositionality, continuity

1

Introduction

Over the last decade a number of researchers have started to develop a theory of structural operational
semantics for probabilistic transition systems (PTSs). Several rule formats for various PTSs were proposed that ensure compositionality of bisimilarity [3, 10, 27] and of approximate bisimilarity [24, 31].
We will consider specifications with rules of the probabilistic GSOS format [3, 9, 29] in order to describe
nondeterministic probabilistic transition systems [30].
Bisimilarity is very sensitive to the exact probabilities of transitions. The slightest perturbation of the
probabilities can destroy bisimilarity. Bisimulation metric [6, 7, 13–16, 25] provides a robust semantics
for probabilistic processes. It is the quantitative analogue to bisimulation equivalence and assigns to
each pair of processes a distance which measures the proximity of their quantitative properties. The
distances form a pseudometric with bisimilar processes at distance 0. Alternative approaches towards a
robust semantics for probabilistic processes are approximate bisimulation [17, 25, 32] and bisimulation
degrees [33]. We consider bisimulation metrics as convincingly argued in e.g. [6, 15, 25].
For compositional specification and reasoning it is necessary that the considered behavioral semantics
is compatible with all operators of the language. For bisimulation metric semantics this is the notion
of uniform continuity. Intuitively, an operator is uniformly continuous if processes composed by that
operator stay close whenever their respective subprocesses are replaced by close subprocesses.
In the 1990s, rule formats that guarantee compositionality of the specified operators have been proposed by (reasonable) argumentation for admissible rules. Prominent examples are the GSOS format [5]
and the ntyft/ntyxt [26] format. More recently, the development of compositional proof systems for the
J. Borgström, S. Crafa (Eds.): Combined Workshop on Expressiveness in
Concurrency and Structural Operational Semantics (EXPRESS/SOS 2014)
EPTCS 160, 2014, pp. 63–78, doi:10.4204/EPTCS.160.7

© D. Gebler & S. Tini
This work is licensed under the
Creative Commons Attribution License.

64

Characterization of Compositionality Properties of Probabilistic Process Combinators

satisfaction relation of HML-formulae [18, 23] allowed to derive rule formats from the logical characterization of the behavioral relation under investigation [4, 19–21].
We propose a new approach that allows to derive for any given specification the compositionality
property of each of its specified operators. The compositionality properties are derived from an appropriate denotational model of the specified language. First, we develop for a concrete process algebra an
appropriate denotational model. The denotation of an open process term describes for each resolution of
the nondeterministic choices how many instances of each process variable are spawned while the process evolves. The number of spawned process replicas is weighted by the likelihood of its realization just
like the bisimulation metric weights the distance between target states by their reachability. We derive
from the denotation of an open process term an upper bound on the bisimulation distance between the
closed instances of the denoted process. Then we generalize this method to arbitrary processes whose
operational semantics is specified by probabilistic GSOS rules. In fact, the upper bound on the bisimulation distance between closed instances of f (x1 , . . . , xr( f ) ) is a modulus of continuity of operator f if the
denotation of f (x1 , . . . , xr( f ) ) is finitely bounded. In this case the operator f is uniformly continuous and
admits for compositional reasoning wrt. bisimulation metric.
This paper continues our research programme towards a theory of robust specifications for probabilistic processes. Earlier work [24] investigated compositional process combinators with respect to approximate bisimulation. Besides the different semantics considered in this paper, we extend substantially
on the approach of [24] by using the newly developed denotational approach. The denotational model
separates clearly between nondeterministic choice, probabilistic choice, and process replication. This
answers also the open question of [24] how the distance of processes composed by process combinators
with a nondeterministic operational semantics can be approximated.

2

Preliminaries

2.1 Probabilistic Transition Systems
A signature is a structure Σ = (F, r), where (i) F is a countable set of operators, and (ii) r : F → N is
a rank function. r( f ) gives the arity of operator f . We write f ∈ Σ for f ∈ F. We assume an infinite
set of state variables Vs disjoint from F. The set of Σ-terms (also called state terms) over V ⊆ Vs ,
notation T (Σ, V), is the least set satisfying: (i) V ⊆ T (Σ, V), and (ii) f (t1 , . . . , tr( f ) ) ∈ T (Σ, V) for f ∈ Σ and
t1 , . . . , tr( f ) ∈ T (Σ, V). T (Σ, ∅) is the set of all closed terms and abbreviated as T(Σ). T (Σ, Vs ) is the set of
open terms and abbreviated as T(Σ). We may refer to operators as process combinators, to variables as
process variables, and to closed terms as processes. Var(t) denotes the set of all state variables in t.
P
Probability distributions are mappings π : T(Σ) → [0, 1] with t∈T(Σ) π(t) = 1 that assign to each closed
term t ∈ T(Σ) its respective probability π(t). By ∆(T(Σ)) we denote the set of all probability distributions
on T(Σ). We let π range over ∆(T(Σ)). The probability mass of T ⊆ T(Σ) in π is defined by π(T ) =
P
i.e., δt (t) = 1 and δt (t′ ) = 0 if t and t′ are
t∈T π(t). Let δt for t ∈ T(Σ) denote the Dirac distribution,
P
syntactically not equal. The convex combination i∈I qi πi of a family {πi }i∈I of probability distributions
P
P
P
πi ∈ ∆(T(Σ)) with qi ∈ (0, 1] and i∈I qi = 1 is defined by ( i∈I qi πi )(t) = i∈I (qi πi (t)). By f (π1 , . . . , πr( f ) )
Qr( f )
we denote the distribution defined by f (π1 , . . . , πr( f ) )( f (t1 , . . . , tr( f ) )) = i=1 πi (ti ). We may write π1 f π2
for f (π1 , π2 ).
In order to describe probabilistic behavior, we need expressions that denote probability distributions. We assume an infinite set of distribution variables Vd . We let µ range over Vd , and x, y range
over V = Vs ∪ Vd . The set of distribution terms over state variables V s ⊆ Vs and distribution variables

D. Gebler & S. Tini

65

Vd ⊆ Vd , notation T (Γ, V s , Vd ) with Γ denoting the signature extending Σ by operators to describe disP
tributions, is the least set satisfying: (i) Vd ∪ {δ(t) | t ∈ T(Σ, V s )} ⊆ T(Γ, V s , Vd ), (ii) i∈I qi θi ∈ T(Γ, V s , Vd )
P
if θi ∈ T(Γ, V s , Vd ) and qi ∈ (0, 1] with i∈I qi = 1, and (iii) f (θ1 , . . . , θr( f ) ) ∈ T(Γ, V s , Vd ) if f ∈ Σ and
θi ∈ T(Γ, V s , Vd ). A distribution variable µ ∈ Vd is a variable that takes values from ∆(T(Σ)). An instantiable Dirac distribution δ(t) is an expression that takes as value the Dirac distribution δt′ when variables
in t are substituted so that t becomes the closed term t′ . Case (ii) allows to construct convex combinations
of distributions. We write θ1 ⊕q θ2 for qθ1 + (1 − q)θ2 . Case (iii) lifts the structural inductive construction
of state terms to distribution terms. T(Γ) denotes T (Γ, Vs , Vd ). Var(θ) denotes the set of all state and
distribution variables in θ.
A substitution is a mapping σ : V → T(Σ) ∪ T(Γ) such that σ(x) ∈ T(Σ) if x ∈ Vs , and σ(µ) ∈ T(Γ)
if µ ∈ Vd . A substitution extends to a mapping from state terms to state terms as usual. A substituP
P
tion extends to distribution terms by σ(δ(t)) = δσ(t) , σ( i∈I qi θi ) = i∈I qi σ(θi ) and σ( f (θ1 , . . . , θr( f ) )) =
f (σ(θ1 ), . . . , σ(θr( f ) )). Notice that closed instances of distribution terms are probability distributions.
Probabilistic transition systems generalize labelled transition systems (LTSs) by allowing for probabilistic choices in the transitions. We consider nondeterministic probabilistic LTSs (Segala-type systems) [30] with countable state spaces.
Definition 1 (PTS) A nondeterministic probabilistic labeled transition system (PTS) is given by a triple
− where Σ is a signature, A is a countable set of actions, and →
− ⊆ T(Σ) × A × ∆(T(Σ)) is a
(T(Σ), A,→),
transition relation.
a

a

a

We write t −
→ π for (t, a, π) ∈ →,
− and t −
→ if t −
→ π for some π ∈ ∆(T(Σ)).

2.2 Specification of Probabilistic Transition Systems
We specify PTSs by SOS rules of the probabilistic GSOS format [3] and adapt from [29] the language
to describe distributions. We do not consider quantitative premises because they are incompatible1 with
compositional approximate reasoning.
Definition 2 (PGSOS rule) A PGSOS rule has the form:
ai,m

{xi −−−→ µi,m | i ∈ I, m ∈ Mi }

bi,n

6 | i ∈ I, n ∈ Ni }
{xi −−−→
a

f (x1 , . . . , xr( f ) ) −
→θ
with I = {1, . . . , r( f )} the indices of the arguments of operator f ∈ Σ, finite index sets Mi , Ni , actions
ai,m , bi,n , a ∈ A, state variables xi ∈ Vs , distribution variables µi,m ∈ Vd , distribution term θ ∈ T(Γ), and
constraints:
1. all µi,m for i ∈ I, m ∈ Mi are pairwise different;
2. all x1 , . . . , xr( f ) are pairwise different;
3. Var(θ) ⊆ {µi,m | i ∈ I, m ∈ Mi } ∪ {x1 . . . , xr( f ) }.
ai,m

bi,n

6 ) above the line are called positive (resp. negative) premises.
The expressions xi −−−→ µi,m (resp. xi −−−→
ai,m

We call µi,m in xi −−−→ µi,m a derivative of xi . We denote the set of positive (resp. negative) premises
a
of rule r by pprem(r) (resp. nprem(r)). The expression f (x1 , . . . , xr( f ) ) −
→ θ below the line is called the
1 Cases 8 and 9 in [24] show that rules with quantitative premises may define operators that are not compositional wrt.
approximate bisimilarity. The same holds for metric bisimilarity.

Characterization of Compositionality Properties of Probabilistic Process Combinators

66

conclusion, notation conc(r), f (x1 , . . . , xr( f ) ) is called the source, notation src(r), the xi are called the
source variables, notation xi ∈ src(r), and θ is called the target, notation trgt(r).
A probabilistic transition system specification (PTSS) in PGSOS format is a triple P = (Σ, A, R),
where Σ is a signature, A is a countable set of actions and R is a countable set of PGSOS rules. R f is
the set of those rules of R with source f (x1 , . . . , xr( f ) ). A supported model of P is a PTS (T(Σ), A,→)
−
a
such that t −
→ π ∈→
− iff for some rule r ∈ R and some closed substitution σ all premises of r hold, i.e.
ai,m

bi,n

ai,m

6 ∈ nprem(r) we have
− and for all xi −−−→
for all xi −−−→ µi,m ∈ pprem(r) we have σ(xi ) −−−→ σ(µi,m ) ∈ →
bi,n

a

σ(xi ) −−−→ π < →
− for all π ∈ ∆(T(Σ)), and the conclusion conc(r) = f (x1 , . . . , xr( f ) ) −
→ θ instantiates to
σ( f (x1 , . . . , xr( f ) )) = t and σ(θ) = π. Each PGSOS PTSS has exactly one supported model [2, 5] which is
moreover finitely branching.

2.3 Bisimulation metric on Probabilistic Transition Systems
Behavioral pseudometrics are the quantitative analogue to behavioral equivalences and formalize the
notion of behavioral distance between processes. A 1-bounded pseudometric is a function d : T(Σ) ×
T(Σ) → [0, 1] with (i) d(t, t) = 0, (ii) d(t, t′ ) = d(t′ , t), and (iii) d(t, t′ ) ≤ d(t, t′′ ) + d(t′′ , t′ ), for all terms
t, t′ , t′′ ∈ T(Σ).
We define now bisimulation metrics as quantitative analogue to bisimulation equivalences. Like for
bisimulation we need to lift the behavioral pseudometric on states T(Σ) to distributions ∆(T(Σ)) and sets
of distributions P(∆(T(Σ))). A matching ω ∈ ∆(T(Σ) × T(Σ)) for (π, π′ ) ∈ ∆(T(Σ)) × ∆(T(Σ)) is given if
P
P
′
′ ′
′
′
t∈T(Σ) ω(t, t ) = π (t ) for all t, t ∈ T(Σ). We denote the set of all matchings
t′ ∈T(Σ) ω(t, t ) = π(t) and
′
′
for (π, π ) by Ω(π, π ). The Kantorovich pseudometric K(d) : ∆(T(Σ)) × ∆(T(Σ)) → [0, 1] is defined for a
pseudometric d : T(Σ) × T(Σ) → [0, 1] by
X
d(t, t′ ) · ω(t, t′ )
K(d)(π, π′ ) = min ′
ω∈Ω(π,π )

t,t′ ∈T(Σ)

for π, π′ ∈ ∆(T(Σ)). The Hausdorff pseudometric H(d̂) : P(∆(T(Σ))) × P(∆(T(Σ))) → [0, 1] is defined for a
pseudometric d̂ : ∆(T(Σ)) × ∆(T(Σ)) → [0, 1] by
(
)
H(d̂)(Π1 , Π2 ) = max sup inf d̂(π1 , π2 ), sup inf d̂(π2 , π1 )
π1 ∈Π1 π2 ∈Π2

π2 ∈Π2 π1 ∈Π1

for Π1 , Π2 ⊆ ∆(T(Σ)) whereby inf ∅ = 1 and sup ∅ = 0.
A bisimulation metric is a pseudometric on states such that for two states each transition from one
state can be mimicked by a transition from the other state and the distance between the target distributions
does not exceed the distance of the source states.
Definition 3 (Bisimulation metric) A 1-bounded pseudometric d on T(Σ) is a bisimulation metric if for
a
a
all t, t′ ∈ T(Σ) with d(t, t′ ) < 1, if t −
→ π′ with K(d)(π, π′ ) ≤ d(t, t′ ).
→ π then there exists a transition t′ −
We order bisimulation metrics d1 ⊑ d2 iff d1 (t, t′ ) ≤ d2 (t, t′ ) for all t, t′ ∈ T(Σ). The smallest bisimulation metric, notation d, is called bisimilarity metric and assigns to each pair of processes the least
possible distance. We call the bisimilarity metric distance also bisimulation distance. Bisimilarity equivalence [28, 30] is the kernel of the bisimilarity metric [13], i.e. d(t, t′ ) = 0 iff t and t′ are bisimilar. We
say that processes t and t′ do not totally disagree if d(t, t′ ) < 1.

D. Gebler & S. Tini

67
a

a

→ for all a ∈ A, i.e. t and t′
Remark 1 Let t, t′ be processes that do not totally disagree. Then t −
→ iff t′ −
agree on the actions they can perform immediately.
Bisimulation metrics can alternatively be defined as prefixed points of a monotone function. Let
([0, 1]T(Σ)×T(Σ) , ⊑) be the complete lattice defined by d ⊑ d′ iff d(t, t′ ) ≤ d′ (t, t′ ), for all t, t′ ∈ T(Σ). We
define the function B : [0, 1]T(Σ)×T(Σ) → [0, 1]T(Σ)×T(Σ) for d : T(Σ) × T(Σ) → [0, 1] and t, t′ ∈ T(Σ) by:

B(d)(t, t′ ) = sup H(K(d))(der(t, a), der(t′ , a))
a∈A

a

with der(t, a) = {π | t −
→ π}.
Proposition 1 ([13]) The bisimilarity metric d is the least fixed point of B.

3

Denotational model

We develop now a denotational model for open terms. Essentially, the denotation of an open term t
describes for each variable in t how many copies are spawned while t evolves. The denotation of t allows
us to formulate an upper bound on the bisimulation distance between closed instances of t. In this section
we consider a concrete process algebra. In the next section we generalize our method to arbitrary PGSOS
specifications.
Let ΣPA be the signature of the core operators of the probabilistic process algebra in [10] defined by
the stop process 0, a family of n-ary prefix operators a.([q1 ] ⊕ · · · ⊕ [qn ] ) with a ∈ A, n ≥ 1, q1 , . . . , qn ∈
Pn
(0, 1] and
Ln i=1 qi = 1, alternative composition + , and parallel composition kB for each B ⊆ A. We
write a. i=1 [qi ] for a.([q1 ] ⊕ · · · ⊕ [qn ] ), and a. for a.[1] (deterministic prefix operator). Moreover,
we write k for kA (synchronous parallel composition). The PTSS PPA = (ΣPA , A, RPA ) is given by
the following PGSOS rules in RPA :
a

a

x2 −
→ µ2

x1 −
→ µ1
a.

n
M

a

[qi ]xi −
→

i=1

a

x1 −
→ µ1

n
X

a

qi δ(xi )

x1 + x2 −
→ µ1

a

x1 + x2 −
→ µ2

i=1

a

x2 −
→ µ2
a

(a ∈ B)

x1 kB x2 −
→ µ1 k B µ2

a

x1 −
→ µ1
a

(a < B)

x1 kB x2 −
→ µ1 kB δ(x2 )

a

x2 −
→ µ2

(a < B)

a

x1 kB x2 −
→ δ(x1 ) kB µ2

We call the open terms T(ΣPA ) nondeterministic probabilistic process terms. We define two important subclasses of T(ΣPA ) that allow for a simpler approximation of the distance of their closed instances.
Let Tdet (ΣPA ) be the set of deterministic process terms, which are those terms of T(ΣPA ) that are built exclusively from the stop process 0, deterministic prefix a. , and synchronous parallel composition k (no
nondeterministic and no probabilistic choices). We call the open terms Tdet (ΣPA ) deterministic because
all probabilistic or nondeterministic choices in the operational semantics of the closed instances σ(t),
with σ : Vs → T(ΣPA ) any closed substitution, arise exclusively from the processes in σ. Let Tprob (ΣPA )
be the set of probabilistic process terms, L
which are those terms of T(ΣPA ) that are built exclusively from
n
the stop process 0, probabilistic prefix a. i=1 [qi ] , and synchronous parallel composition k (no nondeterministic choices). Again, all nondeterministic choices in σ(t) arise exclusively from the processes
in σ.

68

Characterization of Compositionality Properties of Probabilistic Process Combinators

The denotation of a deterministic process term t ∈ Tdet (ΣPA ) is a mapping m : V → N∞ that describes
for each process variable x ∈ Var(t) how many copies of x or some derivative of x are spawned while t
evolves. We call m the multiplicity of t. Let M be the set of all mappings V → N∞ . The denotation
of t, notation ~tM , is defined by ~0M (x) = 0, ~xM (x) = 1, ~xM (y) = 0 if x , y, ~t1 k t2 M (x) =
~t1 M (x) + ~t2 M (x), and ~a.t′ M (x) = ~t′ M (x).
We use notation 0 ∈ M for the multiplicity that assigns 0 to each x ∈ V, and nV ∈ M with V ⊆ V for
the multiplicity such that nV (x) = n if x ∈ V and nV (x) = 0 if x < V. We write nx for n{x} . As it will become
clear in the next sections, we need the denotation m(x) = ∞ for (unbounded) recursion and replication.
We will approximate the bisimulation distance between σ1 (t) and σ2 (t) for closed substitutions
σ1 , σ2 using the denotation of t and the bisimulation distances between processes σ1 (x) and σ2 (x) of
variables x ∈ Var(t). The bisimulation distance of variables is represented by a mapping e : V → [0, 1).
We call e a process distance. Let E be the set of all process distances V → [0, 1). We henceforth assume
closed substitutions σ1 , σ2 with a bisimulation distance between σ1 (x) and σ2 (x) that is strictly less than
1. Practically, this is a very mild restriction because for any (non-trivial) process combinator the composition of processes that totally disagree (i.e. which are in bisimulation distance 1) may lead to composed
processes that again totally disagree. For any d : T(Σ) × T(Σ) → [0, 1] and any closed substitutions σ1 , σ2
we define the associated process distance d(σ1 , σ2 ) ∈ E by d(σ1 , σ2 )(x) = d(σ1 (x), σ2 (x)).
Definition 4 For a multiplicity m ∈ M and process distance e ∈ E we define the deterministic distance
approximation from above as
Y
(1 − e(x))m(x)
D(m, e) = 1 −
x∈V

To understand the functional D remind that e(x) is the distance between processes σ1 (x) and σ2 (x). In
other words, processes σ1 (x) and σ2 (x) disagree by e(x) on their behavior. Hence, σ1 (x) and σ2 (x) agree
Q
by 1 − e(x). Thus, m(x) copies of σ1 (x) and m(x) copies of σ2 (x) agree by at least x∈V (1 − e(x))m(x) ,
Q
and disagree by at most 1 − x∈V (1 − e(x))m(x) .

Example 1 Consider the deterministic process term t = x k x and substitutions σ1 (x) = a.a.0 and σ2 (x) =
a.([0.9]a.0 ⊕ [0.1]0). In this and all following examples we assume that σ1 and σ2 coincide on all other
variables for which the substitution is not explicitly defined, i.e. σ1 (y) = σ2 (y) if x , y in this example. It
is clear that d(σ1 (x), σ2 (x)) = 0.1. Then, d(σ1 (t), σ2 (t)) = 0.1 · 0.9 + 0.9 · 0.1 + 0.1 · 0.1 = 0.19, which is
the likelihood that either the first, the second or both arguments of σ2 (x k x) can perform action a only
once. The denotation of t is ~tM (x) = 2. Then, D(~tM , d(σ1 , σ2 )) = 1 − (1 − 0.1)2 = 0.19.
The functional D defines an upper bound on the bisimulation distance of deterministic processes.
Proposition 2 Let t ∈ Tdet (ΣPA ) be a deterministic process term and σ1 , σ2 be closed substitutions. Then
d(σ1 (t), σ2 (t)) ≤ D(~tM , d(σ1 , σ2 )).
The distance d(σ1 , σ2 ) abstracts from the concrete reactive behavior of terms σ1 (x) and σ2 (x). It
is not hard to see that for deterministic process terms without parallel composition the approximation
functional D gives the exact bisimulation distance. However, the parallel composition of processes may
lead to an overapproximation if the bisimulation distance of process instances arises (at least partially)
from reactive behavior on which the processes cannot synchronize.
Example 2 Consider t = x k a.a.0 and substitutions σ1 (x) = a.b.0 and σ2 (x) = a.([0.9]b.0 ⊕ [0.1]0) with
d(σ1 (x), σ2 (x)) = 0.1. We have d(σ1 (t), σ2 (t)) = 0 since both σ1 (t) and σ2 (t) make an a move to a distribution of parallel compositions either b.0 k a.0 or 0 k a.0 that all cannot proceed. Note that the bisimulation distance between σ1 (x) and σ2 (x) arises from the difference on performing action b which cannot

D. Gebler & S. Tini

69

synchronize with a. The denotation of t is ~tM (x) = 1 which gives in this case an overapproximation of
the distance d(σ1 (t), σ2 (t)) = 0 < D(~tM , d(σ1 , σ2 )) = 1 − (1 − 0.1) = 0.1. However, for σ′1 (x) = a.a.0 and
σ′2 (x) = a.([0.9]a.0 ⊕ [0.1]0) with d(σ′1 (x), σ′2 (x)) = 0.1 we get d(σ′1 (t), σ′2 (t)) = 0.1 = D(~tM , d(σ′1 , σ′2 )).
We remark that the abstraction of the closed substitutions to process distances is intentional and very
much in line with common compositionality criteria that relate the distance of composed processes with
the distance of the process components.
The denotation of a probabilistic process term t ∈ Tprob (ΣPA ) is a distribution p ∈ ∆(M) that describes
for each multiplicity m ∈ M the likelihood p(m) that for each process variable x ∈ Var(t) exactly m(x)
copies of x or some derivative of x are spawned while t evolves. We call p the probabilistic multiplicity
of t. Let P be the set of all distributions ∆(M). The denotation of t, notation ~tP , is defined by
P
~0P = δm with m = 0, ~xP = δm with m = 1x , ~t1 k t2 P (m) =
~t1 P (m1 ) · ~t2 P (m2 ), and
m1 ,m2 ∈M
m(x)=m1 (x)+m2 (x)
for
all
x∈V
Ln
P
~a. i=1 [qi ]ti P = ni=1 qi ~ti P . Notice that ~tP = δ~tM for all t ∈ Tdet (ΣPA ).
For important probabilistic multiplicities we use the same symbols as for multiplicities but it will
always be clear from the context if we refer to probabilistic multiplicities or multiplicities. By 0 ∈ P we
mean the probabilistic multiplicity that gives probability 1 to the multiplicity 0 ∈ M. By nV ∈ P we mean
the probabilistic multiplicity that gives probability 1 to the multiplicity nV ∈ M.
Definition 5 For a probabilistic multiplicity p ∈ P and process distance e ∈ E we define the probabilistic
distance approximation from above as
X
p(m) · D(m, e)
P(p, e) =
m∈M

Example 3 Consider t = a.([0.5](x k x)⊕[0.5]0) and substitutions σ1 (x) = a.a.0 and σ2 (x) = a.([0.9]a.0⊕
[0.1]0) with d(σ1 (x), σ2 (x)) = 0.1. It holds that d(σ1 (t), σ2 (t)) = 0.5(1 − (1 − 0.1)2 ). The probabilistic multiplicity of t is ~tP (2x ) = 0.5 and ~tP (0) = 0.5. Then, D(2x , d(σ1 , σ2 )) = 1 − (1 − 0.1)2 and
D(0, d(σ1 , σ2 )) = 0. Hence, we get the probabilistic distance approximation P(~tP , d(σ1 , σ2 )) = 0.5(1 −
(1 − 0.1)2 ).
Remark 2 The functional P shows a very important interaction between probabilistic choice and process replication. Consider again the process term t = a.([0.5](x k x) ⊕ [0.5]0) and any closed substitutions σ1 , σ2 with d(σ1 (x), σ2 (x)) = ǫ for any ǫ ∈ [0, 1). In the probabilistic distance approximation
P(~tP , d(σ1 , σ2 )) the deterministic distance approximation D(2x , d(σ1 , σ2 )) = 1 − (1 − ǫ)2 of the synchronous parallel execution x k x of two instances of x is weighted by the likelihood 0.5 of its realization.
Hence, P(~tP , d(σ1 , σ2 )) = 0.5(1 − (1 − ǫ)2 ). From Bernoulli’s inequality m1 (1 − (1 − ǫ)n ) ≤ ǫ if m ≥ n, we
get 0.5(1 − (1 − ǫ)2 ) ≤ ǫ. Hence, the distance between instances of two copies running synchronously in
parallel with a probability of 0.5 is at most the distance between those instances running (non-replicated)
with a probability of 1.0.
Notice that P(~tP , d(σ1 , σ2 )) = D(~tM , d(σ1 , σ2 )) for all t ∈ Tdet (ΣPA ). The functional P defines an
upper bound on the bisimulation distance of probabilistic processes.
Proposition 3 Let t ∈ Tprob (ΣPA ) be a probabilistic process term and σ1 , σ2 be closed substitutions. Then
d(σ1 (t), σ2 (t)) ≤ P(~tP , d(σ1 , σ2 )).
Before we can introduce the denotation of nondeterministic probabilistic processes, we need to orP
der the denotation of probabilistic processes. Let π : M → [0, 1] with m∈M π(m) ≤ 1 be a subdistribution over multiplicities. We define the weighting of π as a mapping π : V → R≥0 defined π(x) =

70

Characterization of Compositionality Properties of Probabilistic Process Combinators

P
P
(1/|π|) m∈M π(m) · m(x) if |π| > 0, with |π| = m∈M π(m) the size of π, and π(x) = 0 if |π| = 0. Intuitively,
the number of process copies m(x) are weighted by the probability π(m) of realization of that multiplicity. We order probabilistic multiplicities p1 ⊑ p2 if p1 can be decomposed into subdistributions such that
each multiplicity in p2 is above some weighted subdistribution of p1 . The order is now defined by:
p1 ⊑ p2 iff there is a ω ∈ Ω(p1 , p2 ) with ω(·, m) ⊑ m for all m ∈ M
m1 ⊑ m2 iff m1 (x) ≤ m2 (x) for all x ∈ V
The denotation of a nondeterministic probabilistic process term t ∈ T(ΣPA ) is a set of probabilistic
multiplicities P ⊆ P that describes by p ∈ P some resolution of the nondeterministic choices in t such
that the process evolves as a probabilistic process described by p. We construct a Hoare powerdomain
over the probabilistic multiplicities P and use as canonical representation for any set of probabilistic
multiplicities P ⊆ P the downward closure defined as ↓ P = {p ∈ P | p ⊑ p′ for some p′ ∈ P}. Let D be
the set of non-empty downward closed sets of probabilistic multiplicities {P ⊆ P | P , ∅ and ↓ P = P}. We
use downward closed sets such that D will form a complete lattice with the order defined below (esp.
satisfies antisymmetry, cf. Proposition 4). The denotation of t, notation ~t, is defined by ~0 = {~0P },
~x = ↓ {~xP }, p ∈ ~t1 kB t2  iff there are p1 ∈ ~t1  and p2 ∈L
~t2  such that p ⊑ p′ with p′ defined by
P
n
′
p (m) =
p1 (m1 ) · p2 (m2 ) for all m ∈ M, p ∈ ~a. i=1 [qi ]ti  iff there are pi ∈ ~ti  such that
m1 ,m2 ∈M
m(x)=m1 (x)+m2 (x)
for all x∈V
P
p ⊑ p′ with p′ defined by p′ = ni=1 qi · pi , and ~t1 + t2  = ~t1  ∪ ~t2 . Notice that ~t = ↓ {~tP } for all
t ∈ Tprob (ΣPA ). By 0 ∈ D we mean the singleton set containing the probabilistic multiplicity 0 ∈ P, and
by nV ∈ D the downward closure of the singleton set with element nV ∈ P.
Definition 6 For a nondeterministic probabilistic multiplicity P ∈ D and process distance e ∈ E we define
the nondeterministic probabilistic distance approximation from above as
A(P, e) = sup P(p, e)
p∈P

Example 4 Consider the nondeterministic probabilistic process term t = a.([0.5](x k x) ⊕ [0.5]0) + b.y,
and substitutions σ1 (x) = a.a.0, σ2 (x) = a.([0.9]a.0 ⊕ [0.1]0) and σ1 (y) = b.b.0, σ2 (y) = b.([0.8]b.0 ⊕
[0.2]0). It is clear that d(σ1 (x), σ2 (x)) = 0.1 and d(σ1 (y), σ2 (y)) = 0.2. Now, d(σ1 (t), σ2 (t)) = max{0.5(1−
(1 − 0.1)2 ), 0.2}. The nondeterministic probabilistic multiplicity of t is ~t = ↓ {p1 , p2 }, for p1 (2x ) =
0.5, p1 (0) = 0.5 and p2 (1y ) = 1.0. Thus A(~t, d(σ1 , σ2 )) = max(P(p1 , d(σ1 , σ2 )), P(p2 , d(σ1 , σ2 ))) =
max(0.5(1 − (1 − 0.1)2 ), 0.2).
Notice that A(~t, d(σ1 , σ2 )) = P(~tP , d(σ1 , σ2 )) for all t ∈ Tprob (ΣPA ). Moreover, A(P, e) = A(↓ P, e) for
any P ⊆ P. The functional A defines an upper bound on the bisimulation distance of nondeterministic
probabilistic process terms.
Theorem 1 Let t ∈ T(ΣPA ) be a nondeterministic probabilistic process term and σ1 , σ2 be closed substitutions. Then d(σ1 (t), σ2 (t)) ≤ A(~t, d(σ1 , σ2 )).
Theorem 1 shows that the denotation of a process term is adequate to define an upper bound on the
distance of closed instances of that process term. The converse notion is full-abstraction in the sense
that d(σ1 (t), σ2 (t)) = A(~P, d(σ1 , σ2 )) (no over-approximation). As demonstrated in Example 2, the approximation functionals would require for process variables x ∈ Var(t) besides the bisimulation distance
between σ1 (x) and σ2 (x) also information about the reactive behavior and the branching. However, for
our objective to study the distance of composed processes in relation to the distance of its components,
the bisimulation distance is the right level of abstraction.

D. Gebler & S. Tini

71

We introduce now an order on D that ensures monotonicity of both the approximation functional
A and the functional F introduced in the next section to compute the denotation of arbitrary terms of a
PGSOS PTSS. The order is defined by
P1 ⊑ P2 iff for all p1 ∈ P1 there is a p2 ∈ P2 such that p1 ⊑ p2 .
Proposition 4 (D, ⊑) is a complete lattice.
We order process distances by e1 ⊑ e2 iff e1 (x) ≤ e2 (x) for all x ∈ V. The nondeterministic probabilistic distance approximation A is monotone in both arguments.
Proposition 5 Let P, P′ ∈ D and e, e′ ∈ E. Then A(P, e) ≤ A(P′ , e) if P ⊑ P′ , and A(P, e) ≤ A(P, e′ ) if
e ⊑ e′ .
We will see in the following section that the denotations developed for terms of PPA are sufficient for
terms of any PGSOS PTSS.

4

Distance of composed processes

Now we provide a method to determine the denotation of an arbitrary term. In line with the former section
this gives an upper bound on the bisimulation distance of closed instances of that term. In particular, the
denotation for the term f (x1 , . . . , xr( f ) ) gives an upper bound on the distance of processes composed by
the process combinator f . This allows us in the next section to formulate a simple condition to decide if a
process combinator is uniformly continuous, and hence if we can reason compositionally over processes
combined by that process combinator.

4.1 Operations on process denotations
We start by defining two operations on process denotations that allow us to compute the denotation of
process terms by induction over the term structure. We define the operations first on M and then lift
them to D.
The composition of two processes t1 and t2 which both proceed requires that their multiplicities are
summed up (cf. parallel composition in the prior section). We define the summation of multiplicities by:
(m1 ⊕ m2 )(x) = m1 (x) + m2 (x)
In order to define by structural induction the multiplicity of a term f (t1 , . . . , tr( f ) ), we need an operation
that composes the multiplicity denoting the operator f with the multiplicity of ti . We define the pointed
multiplication of multiplicities with respect to variable y ∈ V by:
(m1 ⊙y m2 )(x) = m1 (y) · m2 (x)
Then, the multiplicity of a state term f (t1 , . . . , tr( f ) ) is given by:
r( f ) 
M

~ f (t1 , . . . , tr( f ) )M =
~ f (x1 , . . . , xr( f ) )M ⊙ xi ~ti M
i=1

Example 5 Consider the open term t = a.x k y. From Section 3 we get ~a.xM = 1x , ~yM = 1y and
~x1 k x2 M = 1{x1 ,x2 } . Then, we have ~tM = (~x1 k x2 M ⊙ x1 ~a.xM ) ⊕ (~x1 k x2 M ⊙ x2 ~yM ) = ((1x1 ⊕
1x2 ) ⊙ x1 1x ) ⊕ ((1x1 ⊕ 1x2 ) ⊙ x2 1y ) = 1{x,y} .

Characterization of Compositionality Properties of Probabilistic Process Combinators

72

It remains to define the multiplicity of f (x1 , . . . , xr( f ) ) for operators f with an operational semantics
defined by some rule r. We define the multiplicity of f (x1 , . . . , xr( f ) ) in terms of the multiplicity of the
target of r. Let µ be a derivative of the source variable x in rule r. We use the property (m ⊙µ 1x )(x) = m(µ)
in order to express the multiplicity m(µ) as a multiplicity of x. Then, the multiplicity of f (x1 , . . . , xr( f ) ) is
defined for any variable x as the summation of the multiplicity of x and its derivatives in the rule target:
!
M
~trgt(r)M ⊙µi,m 1xi
~trgt(r)M ⊕
ai,m

xi

−−−→µi,m ∈
pprem(r)

Example 6 Consider t = f (x) and the following rule r:
a

x−
→µ
a

f (x) −
→µkµ
The operator f mimics the action a of its argument, replicates the derivative µ, and proceeds as a process
that runs two instances of the derivative in parallel. Consider again the closed substitutions σ1 (x) = a.a.0
and σ2 (x) = a.([0.9]a.0 ⊕ [0.1]0) with d(σ1 (x), σ2 (x)) = 0.1. Then, d(σ1 (t), σ2 (t)) = 1 − (1 − 0.1)2 . The
denotation of the target of r is ~trgt(r)M = 2µ . Hence, the denotation of t is 2µ ⊕ (2µ ⊙µ 1x ) = 2{µ,x} . Thus,
D(~tM , d(σ1 , σ2 )) = 1 − (1 − 0.1)2 by d(σ1 , σ2 )(x) = 0.1 and d(σ1 , σ2 )(µ) = 0.
Operations op ∈ {⊕, ⊙y } over M lift to D by
X
(p1 op p2 )(m) =

p1 (m1 ) · p2 (m2 )

m1 ,m2 ∈M
m=m1 op m2

p ∈ (P1 op P2 ) iff ∃p1 ∈ P and p2 ∈ P2 such that p ⊑ p1 op p2

4.2 Approximating the distance of composed processes
Let (Σ, A, R) be any PGSOS PTSS. We compute the denotation of terms and rules as least fixed point of
a monotone function. Let S = S T × S R with S T = T(Σ) ∪ T(Γ) → D and S R = R → D. A pair (τ, ρ) ∈ S
assigns to each term t ∈ T(Σ) ∪ T(Γ) its denotation τ(t) ∈ D and to each rule r ∈ R its denotation ρ(r) ∈ D.
Let S = (S , ⊑) be a poset with ordering (τ, ρ) ⊑ (τ′ , ρ′ ) iff τ(t) ⊑ τ′ (t) and ρ(r) ⊑ ρ′ (r) for all t ∈ T(Σ) ∪ T(Γ)
and r ∈ R. S forms a complete lattice with least element (⊥T , ⊥R ) defined by ⊥T (t) = ⊥R (r) = 0 for all
t ∈ T(Σ) ∪ T(Γ) and r ∈ R.
Proposition 6 S is a complete lattice.
We assume that for all rules r ∈ R the source variable of argument i is called xi . Let Xr be the set
of source variables xi for which r tests the reactive behavior, i.e. xi ∈ Xr iff r has either some positive
ai,m

bi,n

6 .
premise xi −−−→ µi,m or some negative premise xi −−−→
The mapping F : S → S defined in Figure 1 computes iteratively the nondeterministic probabilistic
multiplicities for all terms and rules. As expected, the denotation of a state term f (t1 , . . . , tr( f ) ) is defined
as the application of all rules R f to the denotation of the arguments. However, for distribution terms the
application of the operator needs to consider two peculiarities. First, different states in the support of a
distribution term f (θ1 , . . . , θr( f ) ) may evolve according to different rules of R f .

D. Gebler & S. Tini

73

Function F : S → S is defined by F(τ, ρ) = (τ′ , ρ′ ) with


1x
if t = x







 t = f (t1 , . . . , tr( f ) )
M
r( f )
′
[
τ (t) = 




ρ f ⊙ xi τ(ti )
if  ρ f =

ρ(r)




 i=1
r∈R f



1µ
if θ = µ









τ(t)
if θ = δ(t)




X
X





q
·
τ(θ
)
if
θ
=
qi θi
i
i

τ′ (θ) = 

i∈I
i∈I







 θ = f (θ1 , . . . , θr( f ) )

r( f )

M













if 
ρ f ⊙ xi τ(θi )






sup(sup
ρ(r),
1
)
sup
ρ
=
↓


X
f

r 



i=1


r∈R f
)
(  M

p ⊙µi,m 1xi | p ∈ τ(trgt(r))
ρ′ (r) = p ⊕
ai,m

xi

−−−→µi,m ∈
pprem(r)

Figure 1: Computation of the denotation of arbitrary terms
Example 7 Consider the operator f defined by the following rule:
a

x−
→µ
a

f (x) −
→ µ+µ
Operator f replicates the derivative of x and evolves as alternative composition of both process copies.
Consider the closed substitutions σ1 (x) = a.([0.9]a.a.0 ⊕ [0.1]0) and σ2 (x) = a.([0.9]a.0 ⊕ [0.1]0) with
d(σ1 (x), σ2 (x)) = 0.9. Then, d(σ1 ( f (x)), σ2 ( f (x))) = 1 − 0.12 = 0.99. The denotations for the two rules
defining the alternative composition (see Section 3) are the downward closed sets with maximal elements 1{x1 ,µ1 } and 1{x2 ,µ2 } . Since sup 1{x1 ,µ1 } = 1{x1 ,µ1 } ∈ P, sup 1{x2 ,µ2 } = 1{x2 ,µ2 } ∈ P and 1Xr+ = {x1 },
1
1Xr+ = {x2 } we get ρ+ = ↓ {sup(1{x1 ,µ1 } , 1{x2 ,µ2 } )} = 1{x1 ,x2 ,µ1 ,µ2 } ∈ D. Hence, the denotation for the tar2
get of the f -defining rule is ~µ + µ = (1{x1 ,x2 ,µ1 ,µ2 } ⊙ x1 1µ ) ⊕ (1{x1 ,x2 ,µ1 ,µ2 } ⊙ x2 1µ ) = 2µ . Thus, ~ f (x) = 2x .
Then, D(2x , d(σ1 , σ2 )) = 0.99.
Second, in the distribution term f (θ1 , . . . , θr( f ) ) the operator f may discriminate states in derivatives
belonging to θi solely on the basis that in some rule r ∈ R f the argument xi ∈ Xr gets tested on the ability
to perform or not perform some action.
Example 8 Consider the operators f and g defined by the following rules:
a

x−
→µ
a

f (x) −
→ g(µ)

a

y−
→ µ′
a

g(y) −
→ δ(0)

Operator f mimics the first move of its argument and then, by operator g, only tests the states in the
derivative for their ability to perform action a. Consider first operator g. We get d(σ1 (g(y)), σ2 (g(y))) = 0

74

Characterization of Compositionality Properties of Probabilistic Process Combinators

for all closed substitutions σ1 , σ2 . Clearly, ~g(y) = 0. Consider now t = f (x) and substitutions σ1 (x) =
a.a.0 and σ2 (x) = a.([0.9]a.0 ⊕ [0.1]0) with d(σ1 (x), σ2 (x)) = 0.1. The distance between σ1 ( f (x)) and
σ2 ( f (x)) is the distance between distributions δg(a.0) and 0.9δg(a.0) + 0.1δg(0) . From d(g(a.0), g(0)) = 1 we
get d( f (σ1 (x)), f (σ2 (x))) = K(d)(δg(a.0) , 0.9δg(a.0) + 0.1δg(0) ) = 0.1.
If we would ignore that g tests its argument on the reactive behavior, then the denotation of g(µ)
would be ~g(µ) = ~g(x) ⊙ x 1µ = 0, and the denotation of f (x) would be ~g(µ) ⊕ (~g(µ) ⊙µ 1x ) = 0.
Then D(0, d(σ1 , σ2 )) = 0 < 0.1 = d( f (σ1 (x)), f (σ2 (x))).
Because the operator g tests its argument on the ability to perform action a, it can discriminate instances of the derivative µ the same way as if the process would progress (without replication). Thus, the
denotation of operator g if applied in the rule target is ρg = ↓ {sup(sup 0, 1Xrg )} = 1x as Xrg = {x}. Hence,
~g(µ) = ρg ⊙ x 1µ = 1µ . Thus, ~ f (x) = 1x . It follows, d( f (σ1 (x)), f (σ2 (x))) ≤ D(~ f (x), d(σ1 , σ2 )) = 0.1.
To summarize Examples 7 and 8: The nondeterministic probabilistic multiplicity for operator f applied to some distribution term is given by ρ f = ↓ {supr∈R f sup(sup ρ(r), 1Xr ))} (Figure 1). We explain
this expression stepwise. For any rule r we define by sup ρ(r) ∈ P the least probabilistic multiplicity
which covers all nondeterministic choices represented by the probabilistic multiplicities in ρ(r) ∈ D. By
sup(sup ρ(r), 1Xr ) ∈ P we capture the case that premises of r only test source variables in Xr on their ability to perform an action (Example 8). By supr∈R f sup(sup ρ(r), 1Xr ) ∈ P we define the least probabilistic
multiplicity which covers all choices of rules r ∈ R f (Example 7). Finally, by the downward closure
↓ {supr∈R f sup(sup ρ(r), 1Xr ))} ∈ D we gain the nondeterministic probabilistic multiplicity ρ f that can be
applied to the distribution term (Figure 1).
Proposition 7 F is order-preserving and upward ω-continuous.
From Proposition 6 and 7 and the Knaster-Tarski fixed point theorem we derive the existence and uniqueness of the least fixed point of F. We denote by (ωT , ωR ) the least fixed point of F. We write ~t for ωT (t)
and ~tτ for τ(t). We call ~t the canonical denotation of t. It is not hard to verify that all denotations
presented in Section 3 for PPA are canonical.
A denotation of terms τ ∈ S T is compatible with a distance function d ∈ [0, 1]T(Σ)×T(Σ) , notation d 
~·τ , if d(σ1 (t), σ2 (t)) ≤ A(~tτ , d(σ1 , σ2 )) for all t ∈ T(Σ) and all closed substitutions σ1 , σ2 . Now we
can show that the functional B to compute the bisimulation distance and functional F to compute the
denotations preserve compatibility (Proposition 8). A simple inductive argument allows then to show
that the canonical denotation of terms ~· is compatible with the bisimilarity metric d (Theorem 2).
Proposition 8 Let d ∈ [0, 1]T(Σ)×T(Σ) with d ⊑ B(d) = d′ and (τ, ρ) ∈ S with (τ, ρ) ⊑ F(τ, ρ) = (τ′ , ρ′ ). Then
d  ~·τ implies d′  ~·τ′ .
Theorem 2 Let P be any PGSOS PTSS with d the bisimilarity metric on the associated PTS and ~· the
canonical denotation of terms according to P. Then d  ~·.
Proof sketch. Remind that d is the least fixed point of B : [0, 1]T(Σ)×T(Σ) → [0, 1]T(Σ)×T(Σ) defined by
B(d)(t, t′ ) = supa∈A {H(K(d))(der(t, a), der(t′ , a))} and H the Hausdorff metric functional (Proposition 1).
Let dn = Bn (0) and (τn , ρn ) = Fn (⊥T , ⊥R ). Proposition 8 shows that dn  ~·τn by reasoning inductively
over the transitions specified by the rules. Monotonicity and upward ω-continuity (Proposition 7) ensures
that this property is also preserved in the limit.


5

Compositional Reasoning

In order to reason compositionally over probabilistic processes it is enough if the distance of the composed processes can be related to the distance of their parts. This property is known as uniform continuity.

D. Gebler & S. Tini

75

In essence, compositional reasoning over probabilistic processes is possible whenever a small variance
in the behavior of the parts leads to a bounded small variance in the behavior of the composed processes.
Technically this boils down to the existence of a modulus of continuity. Uniform continuity generalizes
earlier proposals of non-expansiveness [15] and non-extensiveness [1].
Definition 7 (Modulus of continuity) Let f ∈ Σ be any process combinator. A mapping z : [0, 1]r( f ) →
[0, 1] is a modulus of continuity for operator f if z(0, . . . , 0) = 0, z is continuous at (0, . . . , 0), and
′
′
′
d( f (t1 , . . . , tr( f ) ), f (t1′ , . . . , tr(
f ) )) ≤ z(d(t1 , t1 ), . . . , d(tr( f ) , tr( f ) ))

for all closed terms ti , ti′ ∈ T(Σ).
Definition 8 (Uniformly continuous operator) A process combinator f ∈ Σ is uniformly continuous if
f admits a modulus of continuity.
Intuitively, a continuous binary operator f ensures that for any non-zero bisimulation distance ǫ
(understood as the admissible tolerance from the operational behavior of the composed process f (t1 , t2 ))
there are non-zero bisimulation distances δ1 and δ2 (understood as the admissible tolerances from the
operational behavior of the processes t1 and t2 , respectively) such that the distance between the composed
processes f (t1 , t2 ) and f (t1′ , t2′ ) is at most ǫ = z(δ1 , δ2 ) whenever the component t1′ (resp. t2′ ) is in distance
of at most δ1 from t1 (resp. at most δ2 from t2 ). We consider the uniform notion of continuity because
we aim for universal compositionality guarantees.
The denotation of f (x1 , . . . , xr( f ) ) allows to derive a candidate for the modulus of continuity for operator f as follows.
Definition 9 (Derived modulus of continuity) Let P be any PGSOS PTSS. For any operator f ∈ Σ we
define

 r( f )

X
z f (ǫ1 , . . . , ǫr( f ) ) = min  m f (xi )ǫi , 1
i=1

with m f = sup~ f (x1 , . . . , xr( f ) ).

′ )) ≤ z (d(t , t′ ), . . . , d(t
′
Trivially, we have z f (0, . . . , 0) = 0 and d( f (t1 , . . . , tr( f ) ), f (t1′ , . . . , tr(
f
1 1
r( f ) , tr( f ) ))
f)
for all closed terms ti , ti′ ∈ T(Σ) by Theorem 2. However, z f is continuous at (0, . . . , 0) only if the multiplicities in the denotation ~ f (x1 , . . . , xr( f )  assign to each variable a finite value.

Theorem 3 Let P be any PGSOS PTSS. A process combinator f ∈ Σ is uniformly continuous if
~ f (x1 , . . . , xr( f ) ) ⊑ n{x1 ,...,xr( f ) }
for some n ∈ N.
Example 9 We will show that unbounded recursion operators may be not uniformly continuous. We
consider the replication operator of π-calculus specified by the rule:
a

x−
→µ
a

!x −
→ µ k δ(!x)
The replication operator is not continuous since no z with d(!t, !t′ ) ≤ z(d(t, t′ )) and z(0) = 0 will be
continuous at 0 since z(δ) = 1 for any δ > 0. The denotation ~!x = ∞ x shows that the argument x is
infinitely often replicated. Hence, the replication operator is not continuous.

76

Characterization of Compositionality Properties of Probabilistic Process Combinators
Even more, for uniformly continuous operators f the function z f is a modulus of continuity.

Theorem 4 Let P be any PGSOS PTSS. A uniformly continuous process combinator f ∈ Σ satisfies
′
′
′
d( f (t1 , . . . , tr( f ) ), f (t1′ , . . . , tr(
f ) )) ≤ z f (d(t1 , t1 ), . . . , d(tr( f ) , tr( f ) ))

for all closed terms ti , ti′ ∈ T(Σ).
In reverse, for a given modulus of continuity (as specification of some process combinator), we can
derive the maximal replication of process of this operator.
Definition 10 (Derived multiplicity) Let z : [0, 1]n → [0, 1] be a mapping with z(0, . . . , 0) = 0 and z continuous at (0, . . . , 0). Let m : V → R∞
≥0 be defined by


n


X




∞
m = sup 
m
:
V
→
R
|
∀e
∈
E.
m(x
)e(x
)
≤
z(e(x
),
.
.
.
,
e(x
))

i
i
1
n
≥0




i=1

where m1 , m2 : V → R∞
≥0 are ordered m1 ⊑ m2 iff m1 (x) ≤ m2 (x) for all x ∈ V. We call m the derived
multiplicity of z.
Theorem 5 Let P be any PGSOS PTSS, z : [0, 1]n → [0, 1] be a mapping with z(0, . . . , 0) = 0 and z continuous at (0, . . . , 0), and m the derived multiplicity of z. Then, an operator f ∈ Σ with r( f ) = n has z as
modulus of continuity if
sup~ f (x1 , . . . , xr( f ) ) ⊑ m
To conclude, the methods provided in Section 3 and 4 to compute an upper bound on the distance between instances of the term f (x1 , . . . , xr( f ) ) can be used to derive the individual compositionality property
of operator f given by its the modulus of continuity z f . Note that z f depends on all those rules which define operators of processes to which an instance of f (x1 , . . . , xr( f ) ) may evolve to. Traditional rule formats
define syntactic criteria on single rules in order to guarantee a desired compositionality property of the
specified operator. In contrast, our approach derives the compositionality property of an operator from
the the syntactic properties of those rules which define the operational behavior of processes composed
by that operator.

6

Conclusion and Future Work

We presented a method to approximate the bisimulation distance of arbitrary process terms (Theorem 1
and 2). This allows to decide for any given PTSS which operators allow for compositional metric reasoning, i.e. which operators are uniformly continuous (Theorem 3). Moreover, our method allows to
compute for any given PTSS a modulus of continuity of each uniformly continuous operator (Theorem 4). Additionally, for any given modulus of continuity (understood as the required compositionality
property of some operator) we provide a sufficient condition to decide if an operator satisfies the modulus of continuity (Theorem 5). The condition characterizes the maximal number of times that processes
combined by the operator may be replicated during their evolution in order to guarantee the modulus of
continuity.
We will continue this line of research as follows. First, we will investigate the compositionality
of process combinators with respect to convex bisimulation metric [12], discounted bisimulation metric [15], and generalized bisimulation metric [8]. Second, we will explore compositionality with respect

D. Gebler & S. Tini

77

to behavioral pseudometrics based on trace semantics [11] and testing semantics. Finally, we will investigate how the denotational approach to decide the compositionality properties of operators relates to the
logical approach to derive rule formats of [4, 22]. Besides this general line, we want to investigate how
our structural syntactic approach to compositionality relates to the algorithmic computational approach
in [1].

References
[1] Giorgio Bacci, Giovanni Bacci, Kim G Larsen & Radu Mardare (2013): Computing Behavioral Distances,
Compositionally. In: Proc. MFCS’13, Springer, pp. 74–85, doi:10.1007/978-3-642-40313-2_9.
[2] Falk Bartels (2002): GSOS for probabilistic transition systems. In: Proc. CMCS’02, ENTCS 65, Elsevier,
pp. 29–53, doi:10.1016/S1571-0661(04)80358-X.
[3] Falk Bartels (2004): On Generalised Coinduction and Probabilistic Specification Formats. Ph.D. thesis, VU
University Amsterdam.
[4] Bard Bloom, Wan Fokkink & Rob J. van Glabbeek (2004): Precongruence formats for decorated trace
semantics. ACM TOCL 5, pp. 26–78, doi:10.1145/963927.963929.
[5] Bard Bloom, Sorin Istrail & Albert R. Meyer (1995): Bisimulation can’t be traced. J. ACM 42, pp. 232–268,
doi:10.1145/200836.200876.
[6] Franck van Breugel & James Worrell (2005): A Behavioural Pseudometric for Probabilistic Transition Systems. TCS 331(1), pp. 115–142, doi:10.1016/j.tcs.2004.09.035.
[7] Franck van Breugel & James Worrell (2006): Approximating and computing behavioural distances in probabilistic transition systems. TCS 360(1), pp. 373–385, doi:10.1016/j.tcs.2006.05.021.
[8] Konstantinos Chatzikokolakis, Daniel Gebler, Catuscia Palamidessi & Lili Xu: Generalized bisimulation
metrics. In: Proc. CONCUR’14, LNCS, Springer, To appear.
[9] Pedro R. D’Argenio, Daniel Gebler & Matias David Lee (2014): Axiomatizing Bisimulation Equivalences
and Metrics from Probabilistic SOS Rules. In: Proc. FoSSaCS’14, LNCS 8412, Springer, pp. 289–303,
doi:10.1007/978-3-642-54830-7_19.
[10] Pedro R. D’Argenio & Matias David Lee (2012): Probabilistic Transition System Specification: Congruence
and Full Abstraction of Bisimulation. In: Proc. FoSSaCS’12, LNCS 7213, Springer, pp. 452–466, doi:10.
1007/978-3-642-28729-9_30.
[11] L. De Alfaro, M. Faella & M. Stoelinga (2004): Linear and Branching Metrics for Quantitative Transition
Systems. In: Proc. ICALP’04, LNCS 3142, Springer, pp. 97–109, doi:10.1007/978-3-540-27836-8_11.
[12] L. De Alfaro, R. Majumdar, V. Raman & M. Stoelinga (2007): Game relations and metrics.
Proc. LICS’07, IEEE, pp. 99–108, doi:10.1109/LICS.2007.22.

In:

[13] Yuxin Deng, Tom Chothia, Catuscia Palamidessi & Jun Pang (2006): Metrics for Action-labelled Quantitative
Transition Systems. ENTCS 153(2), pp. 79–96, doi:10.1016/j.entcs.2005.10.033.
[14] Yuxin Deng & Wenjie Du (2011): Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation. Technical Report CMU-CS-11-110, CMU.
[15] Josée Desharnais, Vineet Gupta, Radha Jagadeesan & Prakash Panangaden (2004): Metrics for Labelled
Markov Processes. TCS 318(3), pp. 323–354, doi:10.1016/j.tcs.2003.09.013.
[16] Josée Desharnais, Radha Jagadeesan, Vineet Gupta & Prakash Panangaden (2002): The Metric Analogue of
Weak Bisimulation for Probabilistic Processes. In: Proc. LICS’02, IEEE, pp. 413–422, doi:10.1109/LICS.
2002.1029849.
[17] Josée Desharnais, Francois Laviolette & Mathieu Tracol (2008): Approximate Analysis of Probabilistic Processes: Logic, Simulation and Games. In: Proc. QEST’08, IEEE, pp. 264–273, doi:10.1109/QEST.2008.
42.

78

Characterization of Compositionality Properties of Probabilistic Process Combinators

[18] Wan Fokkink, Rob J. van Glabbeek & Paulien de Wind (2006): Compositionality of Hennessy-Milner logic
by structural operational semantics. TCS 354, pp. 421–440, doi:10.1016/j.tcs.2005.11.035.
[19] Wan Fokkink, Rob J. van Glabbeek & Paulien de Wind (2006): Divide and Congruence Applied to ηBisimulation. ENTCS 156, pp. 97–113, doi:10.1016/j.entcs.2005.10.029.
[20] Wan Fokkink, Rob J. van Glabbeek & Paulien de Wind (2006): Divide and Congruence: From Decomposition of Modalities to Preservation of Branching Bisimulation. In: Proc. FMCO’05, LNCS 4111, Springer,
pp. 195–218, doi:10.1007/11804192_10.
[21] Wan Fokkink, Rob J. van Glabbeek & Paulien de Wind (2012): Divide and congruence: From decomposition
of modal formulas to preservation of branching and η-bisimilarity. I&C 214, pp. 59–85, doi:10.1016/j.
ic.2011.10.011.
[22] Maciej Gazda & Wan Fokkink (2010): Congruence from the Operator’s Point of View: Compositionality
Requirements on Process Semantics. In: Proc. SOS’10, EPTCS 32, pp. 15–25, doi:10.4204/EPTCS.32.2.
[23] Daniel Gebler & Wan Fokkink (2012): Compositionality of Probabilistic Hennessy-Milner Logic through
Structural Operational Semantics. In: Proc. CONCUR’12, LNCS 7454, Springer, pp. 395–409, doi:10.
1007/978-3-642-32940-1_28.
[24] Daniel Gebler & Simone Tini (2013): Compositionality of Approximate Bisimulation for Probabilistic Systems. In: Proc. EXPRESS/SOS’13, EPTCS 120, OPA, pp. 32–46, doi:10.4204/EPTCS.120.4.
[25] Alessandro Giacalone, Chi-Chang Jou & Scott A. Smolka (1990): Algebraic Reasoning for Probabilistic
Concurrent Systems. In: Proc. IFIP TC2 Working Conf. on Prog. Concepts and Methods, pp. 443–458.
[26] Jan Friso Groote (1993): Transition System Specifications with Negative Premises. TCS 118(2), pp. 263–299,
doi:10.1016/0304-3975(93)90111-6.
[27] Ruggero Lanotte & Simone Tini (2009): Probabilistic Bisimulation as a Congruence. ACM TOCL 10, pp.
1–48, doi:10.1145/1462179.1462181.
[28] Kim G. Larsen & Arne Skou (1991): Bisimulation Through Probabilistic Testing. I&C 94, pp. 1–28, doi:10.
1016/0890-5401(91)90030-6.
[29] Matias David Lee, Daniel Gebler & Pedro R. D’Argenio (2012): Tree Rules in Probabilistic Transition
System Specifications with Negative and Quantitative Premises. In: Proc. EXPRESS/SOS’12, EPTCS 89,
pp. 115–130, doi:10.4204/EPTCS.89.9.
[30] Roberto Segala (1995): Modeling and Verification of Randomized Distributed Real-Time Systems. Ph.D.
thesis, MIT.
[31] Simone Tini (2010): Non-expansive ǫ-bisimulations for Probabilistic Processes. TCS 411, pp. 2202–2222,
doi:10.1016/j.tcs.2010.01.027.
[32] Mathieu Tracol, Josée Desharnais & Abir Zhioua (2011): Computing Distances between Probabilistic Automata. In: Proc. QAPL’11, EPTCS 57, pp. 148–162, doi:10.4204/EPTCS.57.11.
[33] Mingsheng Ying (2002): Bisimulation indexes and their applications. TCS 275(1), pp. 1–68, doi:10.1016/
S0304-3975(01)00124-4.

