<figure><img src="image_1.png" /></figure>

HAL
open science

# The Theory of Traces for Systems with Nondeterminism, Probability, and Termination

Filippo Bonchi, Ana Sokolova, Valeria Vignudelli

► To cite this version:

Filippo Bonchi, Ana Sokolova, Valeria Vignudelli. The Theory of Traces for Systems with Nondeterminism, Probability, and Termination. Logical Methods in Computer Science, 2022, Volume 18, Issue 2, 10.46298/lmcs-18(2:21)2022. [hal-04856064](https://hal.science/hal-04856064v1)

HAL Id: hal-04856064

https://hal.science/hal-04856064v1

Submitted on 26 Dec 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
THE THEORY OF TRACES FOR SYSTEMS WITH
NONDETERMINISM, PROBABILITY, AND TERMINATION

FILIPPO BONCHI, ANA SOKOLOVA, AND VALERIA VIGNUDELLI

a University of Pisa, Italy

b University of Salzburg, Austria

c Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP, France

ABSTRACT. This paper studies trace-based equivalences for systems combining nondeterministic and probabilistic choices. We show how trace semantics for such processes can be recovered by instantiating a coalgebraic construction known as the generalised powerset construction. We characterise and compare the resulting semantics to known definitions of trace equivalences appearing in the literature. Most of our results are based on the exciting interplay between monads and their presentations via algebraic theories.

# 1. INTRODUCTION

Systems exhibiting both nondeterministic and probabilistic behaviour are abundantly used in verification [BK08, HKK14, KNP02, DJKV17, Var85, Han91, SL95], AI [CPP09, KLC98, RN09], and studied from semantics perspective [HKSH17, SYW$^+$16, HPS$^+$11]. Probability is needed to quantitatively model uncertainty and belief, whereas nondeterminism enables modelling of incomplete information, unknown environment, implementation freedom, or concurrency. At the same time, the interplay of nondeterminism and probability has been posing some remarkable challenges [VW06, KP17, Mio14, Jac08, Var03, Mis00, J.G08, TKP09]. Figure 1 shows a nondeterministic probabilistic system (NPLTS) that we use as a running example.

Traces and trace semantics [Gla01] for nondeterministic probabilistic systems have been studied for several decades within concurrency theory and AI using resolutions or

<footnote>Key words and phrases: probabilistic automata and semantics for probability and nondeterminism and trace semantics and determinisation and coalgebra and convex subsets of distributions monad.</footnote>

<footnote>* This paper is an extended version of a LICS 2019 paper "The Theory of Traces for Systems with Nondeterminism and Probability". It contains all the proofs, additional explanations, material, and examples.</footnote>

<footnote>Filippo Bonchi has been supported by the Ministero dell'Università e della Ricerca of Italy under Grant No. 201784YSZ5, PRIN2017-ASPRA (Analysis of Program Analyses).</footnote>

<footnote>Valeria Vignudelli has been partially supported by the French projects ANR-20-CE48-0005 QuaReMe, the European Research Council (ERC) under the European Union's Horizon 2020 programme (CoVeCe, grant agreement No 678157), the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR).</footnote>
schedulers—entities that resolve the nondeterminism. Most proposals of trace semantics in the literature [Seg95b, Seg95a, BDL14b, BDL14a] are based on such auxiliary notions of resolutions and differ on how these resolutions are defined and combined. We call such approaches *local-view* approaches.

On the other hand, the theory of coalgebra [Rut00, Jac16] provides uniform generic approaches to trace semantics of various kinds of systems and automata, via Kleisli traces [HJS07], generalised determinisation [SBBR10], providing e.g. an abstract treatment of language equivalence for automata, or logics [KR16]. We use the term *global-view* approaches for the coalgebraic methods via generalised determinisation.

In this paper, we propose a theory of trace semantics for nondeterministic probabilistic systems that unifies the local and the global view. We start by taking the global-view approach founded on algebras and coalgebras and inspired by automata theory, and study determinisation of NPLTS in this framework. Then we find a way to mimic the local-view approach and show that we can recover known trace semantics from the literature. We introduce now the main pieces of our puzzle, and show how everything combines together in the theory of traces for NPLTS.

In order to illustrate our approach, it is convenient to recall nondeterministic automata (NDA) and Rabin probabilistic automata (PA) [Rab63]. Both NDA and PA can be described as maps $\langle o, t \rangle: X \to O \times (MX)^A$ where $X$ is a set of states, $A$ is the set of labels, $o: X \to O$ is the output function assigning to each state in $X$ an observation, and $t: X \to (MX)^A$ is the transition function that assigns to each state $x$ in $X$ and to each letter $a$ of the alphabet $A$ an element of $MX$ that describes the choice of a next state. For NDA, this is a nondeterministic choice; for PA, the choice is governed by a probability distribution. An NDA state observes one of two possible values which qualify the state as accepting (output 1) or not (output 0). A state in a PA observes a real number in $[0, 1]$. Below we depict an example NDA (on the left) and an example PA (on the right) with labels $A = \{a, b\}$ and with outputs denoted by $\downarrow$.

<figure><img src="image_3.png" /></figure>

The type of choice, modelled abstractly by a monad $M$, is often linked to a concrete algebraic theory, the presentation of $M$. Having such a presentation is a valuable tool, since it provides a finite syntax for describing finite branching. For nondeterministic choice this is the algebraic theory of semilattices (with bottom), for probabilistic choice it is the algebraic theory of convex algebras. Once we have such an algebraic presentation, we have a determinised automaton (as depicted below) and we inductively compute the output value after executing a trace by following the algebraic structure.

<figure><img src="image_4.png" /></figure>
Here $x \oplus y$ denotes the nondeterministic choice of $x$ or $y$, and $x +_p y$ the probabilistic choice where $x$ is chosen with probability $p$ and $y$ with probability $1-p$. For example, in the determinised PA we have, since $x \xrightarrow{a} x + \frac{1}{2} y$ and $y \xrightarrow{a} y$:

$$x + \frac{1}{2} y \xrightarrow{a} (x + \frac{1}{2} y) + \frac{1}{2} y = x + \frac{1}{4} y$$

and hence the output of $x + \frac{1}{4} y$ is $o(x) + \frac{1}{4} o(y) = \frac{3}{4}$ giving us the probability of $x$ executing the trace *aa*. Our computation is enabled by having the right algebraic structure on the set of observations: a semilattice on $\{0,1\}$ and a convex algebra on $[0,1]$. The induced semantics is language equivalence and probabilistic language equivalence, respectively.

This is the approach of trace semantics via a determinisation [SBBR10], founded in the abstract understanding of automata as coalgebras and computational effects as monads.

We develop a theory of traces for NPLTS using such approach, by first identifying NPLTS as a special class of automata. For this purpose we take the monad for nondeterminism and probability [Jac08] with origins in [Mis00, J.G08, TKP09, Var03, VW06], namely, the monad $C$ of nonempty convex subsets of distributions, and provide all necessary and convenient infrastructure for generalised determinisation. The necessary part is having an algebra of observations, the convenient part is giving an algebraic presentation in terms of convex semilattices. These are algebras that are at the same time a semilattice and a convex algebra, with a distributivity axiom distributing probability over nondeterminism. Having the presentation we can write, for example,

$$x \xrightarrow{a} x_1 \oplus (x_3 + \frac{1}{2} x_2)$$

for the NPLTS from Figure 1.

The presentation for $C$ is somewhat known, although not explicitly proven, in the community — proving it and putting it to good use is part of our contribution which, in our opinion, clarifies and simplifies the trace theory of systems with nondeterminism and probability.

Remarkably, necessity and convenience go hand in hand on this journey. Having the presentation enables us to clearly identify what are the interesting algebras necessary for describing trace and testing semantics (with tests being finite traces). We identify three different algebraic theories: the theory of pointed convex semilattices, the theory of convex semilattices with bottom, and the theory of convex semilattices with top. These theories give rise to three interesting semantics arising in a canonical way by taking as algebras of observations those freely generated by a singleton set. We prove their concrete characterisations: the free convex semilattice with bottom is carried by $[0,1]$ with max as semilattice operation and standard convex algebra operations; the free convex semilattice with top is carried by $[0,1]$ with min as semilattice operation; and the pointed convex semilattice freely generated by 1 is carried by the set of closed intervals in $[0,1]$ where the semilattice operation combines two intervals by taking their minimum and their maximum, and the convex operations are given by Minkowski sum.

We call the resulting three semantics may trace, must trace and may-must trace semantics since there is a close correspondence with probabilistic testing semantics [YL92, JHSY94, DGH+07, DGHM09] when tests are taken to be just the finite traces in $A^*$. Indeed, the may trace semantics gives the greatest probability with which a state passes a given test; the must trace semantics gives the smallest probability with which a state passes a given
<figure><img src="image_5.png" /><figcaption>Figure 1: NPLTS</figcaption></figure>

test, and the may-must trace semantics gives the closed interval ranging from the smallest to the greatest.

From the abstract theory, we additionally get that:

(1) The induced equivalence can be proved coinductively by means of proof-techniques known as *bisimulations up-to* [Mil89]. More precisely, it holds that up-to $\oplus$ and up-to $+_p$ are compatible [PS12] techniques.

(2) The equivalence is implied by the standard branching-time equivalences for NPLTS, namely bisimilarity and convex bisimilarity [SL95, Seg95b].

(3) The equivalence is *backward compatible* w.r.t. trace equivalence for LTS and for reactive probabilistic systems (RPLTS): When regarding an LTS and RPLTS as a nondeterministic probabilistic system, standard trace equivalence coincides with our may trace equivalence and with our three semantics, respectively.

Last but certainly not least, we show that the global view coincides with the local one, namely that our three semantics can be elegantly characterised in terms of resolutions. The may-trace semantics assigns to each trace the greatest probability with which the trace can be performed, with respect to any resolution of the system; the must-trace semantics assigns the smallest one. It is important to remark here that our resolutions differ from those previously proposed in the literature in the fact that they are reactive rather than fully probabilistic. We observe that however this difference does not affect the greatest probability, and we can therefore show that the may-trace coincides with the randomized $\sqcup$-trace equivalence in [Cas18, BDL14b, BDL14a].

Our theory is stated using the language of algebras, coalgebras and, more generally, category theory: this fact, on the one hand, guarantees some sort of canonicity of the constructions we introduce and, on the other, it allows for reusing general results and thus simplifying proofs. Throughout the paper, we make an effort of keeping the presentation as accessible as possible also for those readers which are not familiar with the categorical language.

**Synopsis** We start by illustrating our global-view results concretely, i.e., without relying on categorical notions, in a process algebraic fashion, in Section 2. We recall monads and algebraic theories in Section 3. We provide a presentation for the monad *C* in Section 4
$$ \frac{-}{x \xrightarrow{a} \text{term}_X(t(x)(a))} \quad \frac{-}{\star \xrightarrow{a} \star} \quad \frac{s_1 \xrightarrow{a} s'_1 \quad s_2 \xrightarrow{a} s'_2}{s_1 \oplus s_2 \xrightarrow{a} s'_1 \oplus s'_2} \quad \frac{s_1 \xrightarrow{a} s'_1 \quad s_2 \xrightarrow{a} s'_2}{s_1 +_p s_2 \xrightarrow{a} s'_1 +_p s'_2} $$
(a) Transition function.

$$ \frac{-}{x \downarrow_1} \quad \frac{-}{\star \downarrow_0} \quad \frac{s_1 \downarrow_{o_1} \quad s_2 \downarrow_{o_2}}{s_1 \oplus s_2 \downarrow_{\max(o_1,o_2)}} \quad \frac{s_1 \downarrow_{o_1} \quad s_2 \downarrow_{o_2}}{s_1 +_p s_2 \downarrow_{p \cdot o_1 + (1-p) \cdot o_2}} $$

(b) Output function for may trace ($\equiv_B$): $o_1, o_2 \in [0, 1]$.

$$ \frac{-}{x \downarrow_1} \quad \frac{-}{\star \downarrow_0} \quad \frac{s_1 \downarrow_{o_1} \quad s_2 \downarrow_{o_2}}{s_1 \oplus s_2 \downarrow_{\min(o_1,o_2)}} \quad \frac{s_1 \downarrow_{o_1} \quad s_2 \downarrow_{o_2}}{s_1 +_p s_2 \downarrow_{p \cdot o_1 + (1-p) \cdot o_2}} $$

(c) Output function for must trace ($\equiv_T$): $o_1, o_2 \in [0, 1]$.

$$ \frac{-}{x \downarrow_{[1,1]}} \quad \frac{-}{\star \downarrow_{[0,0]}} \quad \frac{s_1 \downarrow_{o_1} \quad s_2 \downarrow_{o_2}}{s_1 \oplus s_2 \downarrow_{\min-\max(o_1,o_2)}} \quad \frac{s_1 \downarrow_{o_1} \quad s_2 \downarrow_{o_2}}{s_1 +_p s_2 \downarrow_{o_1 +_p o_2}} $$

(d) Output function for may-must trace ($\equiv$): $o_1, o_2 \in \mathcal{J} = \{[x, y] \mid x, y \in [0, 1] \wedge x \le y\}$. For all $[x_1, y_1], [x_2, y_2] \in \mathcal{J}$, $\min-\max([x_1, y_1], [x_2, y_2]) = [\min(x_1, x_2), \max(y_1, y_2)]$ and $[x_1, y_1] +_p^j [x_2, y_2] = [p \cdot x_1 + (1-p) \cdot x_2, p \cdot y_1 + (1-p) \cdot y_2]$.

<caption>Table 1: Structural Operational Semantics (GSOS) for NPLTS.</caption>

(Theorem 4.7) and combine it with termination in Section 5. We then recall, in Section 6, the generalised determinisation and show an additional useful result (Theorem 6.8). All these pieces are put together in Section 7, where we introduce our three semantics and discuss their properties. The correspondence of the global view with the local one is illustrated in Section 8 (Theorem 8.4).

## 2. TRACE SEMANTICS FOR NPLTS, CONCRETELY

A nondeterministic probabilistic transition system with labels in $A$ is a pair $(X, t)$ where $X$ is the set of states and $t: X \to (\mathcal{P}\mathcal{D}X)^A$ is a function assigning to each state $x \in X$ and label $a \in A$ a set of probability distributions over $X$.<fnref n="1" />

The idea is to construct for each NPLTS $(X, t)$, a process calculus where the states in $X$ act as constants and the behaviour of such constants is determined by $t$. The terms of the calculus are defined inductively by the following grammar.

$$ s ::= x \in X \mid \star \mid s \oplus s \mid s +_p s \quad \text{for all } p \in [0, 1] $$

The inference rules in Table 1.(a) define a transition function over the terms of this grammar. The rules for $\star, \oplus$ and $+_p$ are self-explanatory. The rule for the constants $x \in X$ requires some explanation: the transitions of $x$ are defined using the transition function $t$ of the original NPLTS. Observe that for $a \in A$, $t(x)(a)$ is an element of $\mathcal{P}\mathcal{D}X$. The function $\text{term}_X$ assigns to each of these elements its representation as term of the grammar. Indeed,

<footnote n="1">¹To be completely precise, we should say a finite set of finitely supported distributions. This will be explained in full details in Section 3.</footnote>
sets of distributions, namely the elements of $\mathcal{PDX}$, can be represented by the syntax above: distributions are represented by terms of the shape $(...((x_0 + p_0 x_1) + p_2 x_2)...)+_{p_n} x_n$; sets of probability distributions by terms of the shape $(... (d_0 \oplus d_1) \oplus d_{n-1})... \oplus d_n$ where each $d_i$ is a term representing a distribution. The empty set is represented by $\star$.

For instance, when starting with the NPLTS in the left of Figure 1, the axiom for constants get instantiated to the following transitions:

$$ 
\begin{array}{ccc}
x \xrightarrow{a} x_1 \oplus (x_2 + \frac{1}{2} x_3) & x \xrightarrow{b} \star & x \xrightarrow{c} \star \\
x_1 \xrightarrow{a} \star & x_1 \xrightarrow{b} x + \frac{1}{2} x_3 & x_1 \xrightarrow{c} \star \\
x_2 \xrightarrow{a} \star & x_2 \xrightarrow{b} x_3 & x_2 \xrightarrow{c} x \\
x_3 \xrightarrow{a} \star & x_3 \xrightarrow{b} \star & x_3 \xrightarrow{c} \star
\end{array}
$$

Note that $x \xrightarrow{a} \star$ means $x \not\stackrel{a}{\to}$, i.e. $x$ cannot perform a transition with label $a$. Now, with these axioms and the three other rules in Table 1(a) one can compute transitions for arbitrary terms of the syntax. For instance, starting from $x$, one obtains the transition system partially depicted below.

<figure><img src="image_6.png" /></figure>

It is important to note that this transition systems is deterministic: for each term $s$ and for each letter $a \in A$, there exists exactly one term $s'$ such that $s \xrightarrow{a} s'$. Therefore, for each word $w \in A^*$, there exists exactly one term reachable from $s$ with $w$. We denote this term by $t_w(s)$.

Furthermore, in order to define trace semantics, we decorate each term $s$ with an output value: the trace semantics of $s$, written $\llbracket s \rrbracket$, is the function that maps each word $w \in A^*$ into the output value of $t_w(s)$. In Table 1(b),(c),(d), we define three different ways of decorating terms with outputs: we write $s \downarrow_o$ to mean that the output of $s$ is $o$. These three different ways lead to three different trace semantics: may ($\equiv_B$), must ($\equiv_T$) and may-must ($\equiv$).

For instance, the may trace and the must trace semantics of $x$ from Figure 1 are partially depicted as on the left and, respectively, on the right below.

$$ 
\begin{array}{l@{\qquad}l}
\varepsilon & \mapsto 1 \\
a & \mapsto 1 \\
b & \mapsto 0 \\
c & \mapsto 0 \\
aa & \mapsto 0 \\
ab & \mapsto 1 \\
ac & \mapsto \frac{1}{2} \\
\dots & \mapsto \dots
\end{array}
\qquad
\begin{array}{l@{\qquad}l}
\varepsilon & \mapsto 1 \\
a & \mapsto 1 \\
b & \mapsto 0 \\
c & \mapsto 0 \\
aa & \mapsto 0 \\
ab & \mapsto \frac{1}{2} \\
ac & \mapsto 0 \\
\dots & \mapsto \dots
\end{array}
$$
In the rest of the paper we study the three semantics that we have described so far. Our abstract treatment provides an explanation for each element of the above construction: all design choices of this semantics have a mathematical justification and nothing is arbitrary. Moreover, these semantics enjoy many desirable properties that can be easily proven by means of our abstract construction. We will come back to NPLTS and these trace semantics in Section 7, but first we need to set up the necessary algebraic (Sections 3, 4 and 5) and coalgebraic (Section 6) playground.

### 3. MONADS AND ALGEBRAIC THEORIES

In this paper, on the algebraic side, we deal with Eilenberg-Moore algebras of a monad on the category **Sets** of sets and functions, for which we also give presentations in terms of operations and equations, i.e., algebraic theories.

**3.1. Monads.** A monad on **Sets** is a functor $M: \mathbf{Sets} \to \mathbf{Sets}$ together with two natural transformations: a unit $\eta: \mathrm{Id} \Rightarrow M$ and multiplication $\mu: M^2 \Rightarrow M$ that satisfy the laws

<figure><img src="image_7.png" /></figure>

We next introduce several monads on **Sets**, relevant to this paper. Each monad can be seen as giving side-effects.

**Nondeterminism** The finite powerset monad $\mathcal{P}$ maps a set $X$ to its finite powerset $\mathcal{P}X = \{U \mid U \subseteq X, U \text{ is finite}\}$ and a function $f: X \to Y$ to $\mathcal{P}f: \mathcal{P}X \to \mathcal{P}Y$, $\mathcal{P}f(U) = \{f(u) \mid u \in U\}$. The unit $\eta$ of $\mathcal{P}$ is given by singleton, i.e., $\eta(x) = \{x\}$ and the multiplication $\mu$ is given by union, i.e., $\mu(S) = \bigcup_{U \in S} U$ for $S \in \mathcal{P}\mathcal{P}X$. Of particular interest to us in this paper is the submonad $\mathcal{P}_{ne}$ of non-empty finite subsets, that acts on functions just like the (finite) powerset monad, and has the same unit and multiplication. We rarely mention the unrestricted (not necessarily finite) powerset monad, which we denote by $\mathcal{P}_u$. We sometimes write $\bar{f}$ for $\mathcal{P}_u f$ in this paper.

**Probability** The finitely supported probability distribution monad $\mathcal{D}$ is defined, for a set $X$ and a function $f: X \to Y$, as

$$ \mathcal{D}X = \{\varphi: X \to [0,1] \mid \sum_{x \in X} \varphi(x) = 1, \mathrm{supp}(\varphi) \text{ is finite}\} $$

$$ \mathcal{D}f(\varphi)(y) = \sum_{x \in f^{-1}(y)} \varphi(x). $$

The support set of a distribution $\varphi \in \mathcal{D}X$ is $\mathrm{supp}(\varphi) = \{x \in X \mid \varphi(x) \neq 0\}$. The unit of $\mathcal{D}$ is given by a Dirac distribution $\eta(x) = \delta_x = (x \mapsto 1)$ for $x \in X$ and the multiplication by $\mu(\Phi)(x) = \sum_{\varphi \in \mathrm{supp}(\Phi)} \Phi(\varphi) \cdot \varphi(x)$ for $\Phi \in \mathcal{D}\mathcal{D}X$. We sometimes write $\sum_{i \in I} p_i x_i$ for a distribution $\varphi$ with $\mathrm{supp}(\varphi) = \{x_i \mid i \in I\}$ and $\varphi(x_i) = p_i$.
**Termination** The termination monad, also called lift and denoted by $\cdot + 1$ maps a set $X$ to the set $X+1$, where $+$ denotes the coproduct in **Sets**, which amounts to disjoint union, and $1 = \{\star\}$. For a coproduct $A+B$ we write $in_l: A \to A+B$ and $in_r: B \to A+B$ for the left and right coproduct injections, respectively. This monad maps a function $f: X \to Y$ to the function $f+1: X+1 \to Y+1$ defined, as expected, by $(f+1)(in_l(x)) = in_l(f(x))$ for $x \in X$ and $(f+1)(in_r(\star)) = in_r(\star)$. The unit of the termination monad is given by the left injection, $\eta: X \to X+1$ with $\eta(x) = in_l(x)$ and the multiplication by $\mu(in_l \circ in_l(x)) = in_l(x)$ for $x \in X$, $\mu(in_l \circ in_r(\star)) = in_r(\star)$, and $\mu(in_r(\star)) = in_r(\star)$. If clear from the context, we may omit explicit mentioning of the injections, and write for example $(f+1)(x) = x$ for $x \in X$ and $(f+1)(\star) = \star$.

**3.2. Monad Maps, Quotients and Submonads.** A monad map from a monad $M$ to a monad $\hat{M}$ is a natural transformation $\sigma: M \Rightarrow \hat{M}$ that makes the following diagrams commute, with $\eta, \mu$ and $\hat{\eta}, \hat{\mu}$ denoting the unit and multiplication of $M$ and $\hat{M}$, respectively, and $\sigma\sigma$ denoting $\sigma\hat{M} \circ M\sigma = \hat{M}\sigma \circ \sigma M$.

<figure><img src="image_8.png" /></figure>

If $\sigma: M \Rightarrow \hat{M}$ is an epi monad map, then $\hat{M}$ is a quotient of $M$. If it is a mono, then $M$ is a submonad of $\hat{M}$. If it is an iso, the two monads are isomorphic.

**3.3. Distributive Laws.** Let $(M, \eta, \mu)$ be a monad and $F$ a functor. A natural transformation $\lambda: MF \Rightarrow FM$ is a functor distributive law of the monad $M$ over the functor $F$ if it commutes appropriately with the unit and the multiplication of $M$, i.e.,

<figure><img src="image_9.png" /></figure>

Let $(M, \eta, \mu)$ and $(\hat{M}, \hat{\eta}, \hat{\mu})$ be two monads. A monad distributive law of $M$ over $\hat{M}$ is a natural transformation $\lambda: M\hat{M} \Rightarrow \hat{M}M$ that commutes appropriately with the units and the multiplications of the monads, i.e.,

<figure><img src="image_10.png" /></figure>

and

<figure><img src="image_11.png" /></figure>
Given a monad distributive law $\lambda: M\hat{M} \Rightarrow \hat{M}M$, we get a composite monad $\bar{M} = \hat{M}M$ with unit $\bar{\eta} = \hat{\eta}\eta$ and multiplication $\bar{\mu} = \hat{\mu}\mu \circ \hat{M}\lambda M$.

For any monad $M$ on Sets, there exists a distributive law $\iota: M + 1 \Rightarrow M(\cdot + 1)$ defined as

$$ \iota_X = (MX + 1 \xrightarrow{[Min_l, \eta_{X+1} \circ in_r]} M(X + 1)). \quad (3.1) $$

As a consequence, $M(\cdot + 1)$ is a monad. Moreover, we get the following useful property.

**Lemma 3.1.** Whenever $\sigma: M \Rightarrow \hat{M}$ is a monad map, also $\sigma(\cdot + 1): M(\cdot + 1) \Rightarrow \hat{M}(\cdot + 1)$ is a monad map. Injectivity of $\sigma$ implies injectivity of $\sigma(\cdot + 1)$. $\square$

Lemma 3.1 follows directly from Lemma 3.3 and Lemma 3.4 below. Before we state and prove these, let us consider another example of a distributive law in the other direction.

**Example 3.2.** We have that $\mathcal{D} + 1$ is a monad, since $\beta: \mathcal{D}(\cdot + 1) \Rightarrow \mathcal{D} + 1$ given by

$$ \beta(\varphi) = \left\{ \begin{array}{ll} \varphi_X & * \notin \text{supp}(\varphi) \wedge \forall x \in X. \varphi_X(x) = \varphi(in_l(x)) \\ * & * \in \text{supp}(\varphi) \end{array} \right. $$

is a monad distributive law. This $\beta$ corresponds to termination as a “black-hole” of [SW18].

**Lemma 3.3.** Given three monads $M$, $\hat{M}$, and $T$, two monad distributive laws $\lambda: TM \Rightarrow MT$ and $\bar{\lambda}: T\hat{M} \Rightarrow \hat{MT}$, ensuring that $MT$ and $\hat{MT}$ are monads, and a monad map $\sigma: M \Rightarrow \hat{M}$. If the following diagram commutes, in which case we say that $\sigma$ is a map of distributive laws,

<figure><img src="image_12.png" /></figure>

then $\sigma T: MT \Rightarrow \hat{MT}$ is a monad map. If $\sigma$ is injective, then $\sigma T$ is as well.

*Proof.* We denote by $\eta, \mu$ the unit and multiplication of $M$, by $\hat{\eta}, \hat{\mu}$ those of $\hat{M}$ and by $\eta^T, \mu^T$ those of $T$. Note that $\sigma T_X = \sigma_{TX}$ and hence, using that $\sigma$ is a monad map, we get immediately $\sigma T_X \circ \eta_{TX} \circ \eta_X^T = \hat{\eta}_{TX} \circ \eta_X^T$.

The following diagram commutes since $\sigma$ is a monad map.

$$ \begin{tikzcd} MMTX \arrow[r, "\sigma^{MT}"] \arrow[d, "\mu T"] & \hat{M}MTX \arrow[r, "\hat{M}\sigma T"] \arrow[d, "\hat{\mu} T"] & \hat{M}\hat{M}TX \arrow[d, "\sigma T"] \\ MTX & & \hat{M}TX \arrow[r, "\sigma T"] & \hat{M}TX \arrow[d, "\mu T"] \end{tikzcd} \quad (3.2) $$

From the naturality of $\sigma$, the following diagram also commutes.

$$ \begin{tikzcd} MMTTX \arrow[r, "\sigma^{MTT}"] \arrow[d, "MM\mu^T"] & \hat{M}MTTX \arrow[r, "\hat{M}\sigma^{TT}"] \arrow[d, "\hat{M}M\mu^T"] & \hat{M}\hat{M}TTX \arrow[d, "\hat{M}\hat{M}\mu^T"] \\ MMTX & & \hat{M}MTX \arrow[r, "\sigma^{MT}"] \arrow[d, "\sigma^{MT}"] \arrow[r, "\hat{M}\sigma^{TT}"] \arrow[d, "\hat{M}\hat{M}\mu^T"] \arrow[r, "\sigma^{MTT}"] \arrow[d, "\sigma^{MTT}"] \arrow[r, "\sigma^{TT}"] \arrow[d, "\sigma^{TT}"] \end{tikzcd} \quad (3.3) $$

Using once again the naturality of $\sigma$, for the left square, and the assumption that $\sigma$ is a map of distributive laws, for the square on the right, we get the commutativity of the following
### 3.4. Algebraic Theories.
With a monad $M$ one associates the Eilenberg-Moore category EM($M$) of $M$-algebras. Objects of EM($M$) are pairs $\mathbb{A} = (A, a)$ of a set $A \in \textbf{Sets}$ and a map $a: MA \to A$, making the first two diagrams below commute.

<figure><img src="image_13.png" /></figure>

A homomorphism from an algebra $\mathbb{A} = (A, a)$ to an algebra $\mathbb{B} = (B, b)$ is a map $h: A \to B$ between the underlying sets making the third diagram above commute. Hence the second diagram tells us that $a$ is a homomorphism from $(MA, \mu)$ to $(A, a)$. It is direct to check that $(MA, \mu)$ is an Eilenberg-Moore algebra. Moreover, $(MA, \mu)$ the free Eilenberg-Moore algebra generated by $A$.

In this paper we care for both categorical algebra, algebras of a monad, and their presentations in terms of algebraic theories and their models. An algebraic theory is a pair $(\Sigma, E)$ of signature $\Sigma$ (a set of operation symbols) and a set of equations $E$ (a set of pairs of terms). A $(\Sigma, E)$-algebra, or a model of the algebraic theory $(\Sigma, E)$ is an algebra $\mathbb{A} = (A, \Sigma_A)$ with carrier set $A$ and a set of operations $\Sigma_A$, one for each operation symbol in $\Sigma$, that satisfies the equations in $E$. A homomorphism from a $(\Sigma, E)$-algebra $\mathbb{A} = (A, \Sigma_A)$ to a $(\Sigma, E)$-algebra $\mathbb{B} = (B, \Sigma_B)$ is a function $h: A \to B$ that commutes with the operations, i.e., $h \circ f_A = f_B \circ h^n$ for all $n$-ary $f \in \Sigma$, and $f_A, f_B$ its interpretations in $\mathbb{A}, \mathbb{B}$, respectively. $(\Sigma, E)$-algebras together with their homomorphisms form a category.

Every algebraic theory gives rise to a monad, defined by the free $\mathbb{1}$ forgetful adjunction, see e.g. [Mac71, V.6]. We now explicitly recall the construction. In this construction, free algebras play an important role. Recall that $\mathbb{F}_X = (FX, \Sigma_{FX})$ is the free $(\Sigma, E)$-algebra generated by $X \subseteq FX$ if for any $(\Sigma, E)$-algebra $\mathbb{A} = (A, \Sigma_A)$, any function $f: X \to A$ extends to a unique homomorphism $f^\# : \mathbb{F}_X \to \mathbb{A}$. Free algebras are unique up to isomorphism. For any set $X$, the free $(\Sigma, E)$-algebra generated by $X$ is isomorphic to the algebra with carrier the set of $\Sigma$-terms with variable in $X$ modulo $E$-equations. The adjunction give rise to the monad $T_{\Sigma,E}$ of $\Sigma$-terms modulo $E$-equations. We next describe this monad.

Given a signature $\Sigma$, the monad $T_\Sigma$ of $\Sigma$-terms maps a set $X$ to the set of all $\Sigma$-terms with variables in $X$, and $f: X \to Y$ to the function that maps a term over $X$ to a term over $Y$ obtained by substitution according to $f$. The unit maps a variable in $X$ to itself, and the multiplication is term composition. Given an algebraic theory $(\Sigma, E)$, the monad $T_{\Sigma,E}$ of $\Sigma$-terms modulo $E$-equations is defined analogously, using equivalence classes of terms rather than plain terms. The monad $T_{\Sigma,E}$ is a quotient of $T_\Sigma$. Moreover, for two sets of equations $E_1 \subseteq E_2$, the monad $T_{\Sigma,E_2}$ is a quotient of $T_{\Sigma,E_1}$.

**Definition 3.5.** A *presentation* of a monad $M$ is an algebraic theory $(\Sigma, E)$ such that the monad $T_{\Sigma,E}$ is isomorphic to $M$.

Clearly, $(\Sigma, E)$ is a presentation of the monad $T_{\Sigma,E}$.

**Remark 3.6.** A direct, syntactic, way to prove that $(\Sigma, E)$ is a presentation of a monad $M$ is to provide a monad isomorphism from $T_{\Sigma,E}$ to $M$. We give such a direct syntactic proof for our monad of interest in [BSV21]. We now briefly discuss other ways to prove that $(\Sigma, E)$ presents $M$, which justify our proof of the presentation in this paper (Theorem 4.7).

Let $U: \mathbf{A} \to \mathbf{Sets}$ be the forgetful functor from the category $\mathbf{A}$ of $(\Sigma, E)$-algebras to $\mathbf{Sets}$ and let $F_{\Sigma,E}$ be the left adjoint to $U$ mapping a set $X$ to the $(\Sigma, E)$-algebra of $\Sigma$-terms
modulo E-equations. We have $T_{\Sigma,E} = UF_{\Sigma,E}$. Now, suppose that $F$ is another left adjoint to $U$. Since adjoints are unique up to isomorphism, there exists an isomorphism $\iota: F_{\Sigma,E} \Rightarrow F$. It is not difficult to derive from this that $U\iota: UF_{\Sigma,E} \Rightarrow UF$ is an isomorphism from the monad $T_{\Sigma,E} = UF_{\Sigma,E}$ to the monad $UF$. Hence, in order to prove that $(\Sigma, E)$ presents a monad $M$, it suffices to show that there exists some left adjoint $F$ to the forgetful functor $U$ such that $M = UF$. This is what we use to prove the presentation in this paper, in the proof of Proposition 4.3 below. The proposition itself identifies sufficient conditions for $M = UF$ to hold, for an adjoint $F$ to the forgetful functor $U$.

One can also work on the level of the categories of algebras. The main observation is the following: a monad $M$ is isomorphic to a monad $T$ if and only if there is a concrete isomorphism $I$ between their categories of Eilenberg-Moore algebras, as in the following diagram:

<figure><img src="image_14.png" /></figure>

In such a case, using uniqueness of adjoints up to isomorphism, we also have an isomorphism $\iota: F^T \Rightarrow IF^M$ with $F^M$ and $F^T$ being the left adjoints of the forgetful functors $U^M$ and $U^T$, respectively, and the monad isomorphism is given by

$$M = U^M F^M = U^T I F^M \stackrel{U^T \iota^{-1}}{\implies} U^T F^T = T.$$

In the other direction, given a monad isomorphism $\sigma: M \Rightarrow T$, we have that

<figure><img src="image_15.png" /></figure>

is a concrete isomorphism of the algebras. Hence, another way to prove that $(\Sigma, E)$ is a presentation of $M$ is to provide a concrete isomorphism between $EM(T_{\Sigma,E})$ and $EM(M)$.

Moreover, as a consequence of Beck's theorem (see [Mac71, Theorem VI.8.1]), there is a concrete isomorphism between $(\Sigma, E)$-algebras and $EM(T_{\Sigma,E})$ given by the comparison functor. Hence we get that $(\Sigma, E)$ is a presentation of $M$ if and only if there is a concrete isomorphism between the category of $(\Sigma, E)$-algebras and $EM(M)$. This leads us to a third way to prove that $(\Sigma, E)$ is a presentation of $M$: providing a concrete isomorphism between $(\Sigma, E)$-algebras and $EM(M)$. This way of providing a presentation was used in [MV20, MSV21].

Such concrete isomorphism can be also obtained using again [Mac71, Theorem VI.8.1]. The theorem states that if $M$ is the monad that arises from an adjunction $F \dashv U$ for the forgetful functor $U: A \to \mathbf{Sets}$, then the comparison functor provides a concrete isomorphism

<footnote n="2">²We thank Aloïs Rosset for reminding us of the necessity of a concrete isomorphism. Previous versions of this paper omitted mentioning that the isomorphism needs to be concrete, although our presentation proofs were not affected by this.</footnote>
from $(\Sigma, E)$-algebras to EM($M$). Hence, our proof of the presentation using Proposition 4.3 can also be (indirectly) justified this way.

In the sequel, we present several algebraic theories that give presentations to the monads of interest.

**Presenting the monad $\mathcal{P}_{ne}$** Let $\Sigma_N$ be the signature consisting of a binary operation $\oplus$. Let $E_N$ be the following set of axioms, stating that $\oplus$ is associative, commutative, and idempotent, respectively.

$$ 
\begin{array}{ccc}
(x \oplus y) \oplus z & \stackrel{(A)}{=} & x \oplus (y \oplus z) \\
x \oplus y & \stackrel{(C)}{=} & y \oplus x \\
x \oplus x & \stackrel{(I)}{=} & x
\end{array}
 $$

The algebraic theory $(\Sigma_N, E_N)$ of *semilattices* provides a presentation for the monad $\mathcal{P}_{ne}$. We refer to this theory as the theory of nondeterminism. To avoid confusion later, it is convenient to fix here the interpretation of $\oplus$ as a join (rather than a meet) and, thus, to think of the induced order as $x \sqsubseteq y$ iff $x \oplus y = y$.

**Presenting the monad $\mathcal{D}$** Let $\Sigma_P$ be the signature consisting of binary operations $+_p$ for all $p \in (0, 1)$. Let $E_P$ be the following set of axioms.

$$ 
\begin{array}{ccc}
(x +_q y) +_p z & \stackrel{(A_p)}{=} & x +_{pq} (y +_{\frac{p(1-q)}{1-pq}} z) \\
x +_p y & \stackrel{(C_p)}{=} & y +_{1-p} x \\
x +_p x & \stackrel{(I_p)}{=} & x
\end{array}
 $$

Here, $(A_p)$, $(C_p)$, and $(I_p)$ are the axioms of parametric associativity, commutativity, and idempotence. The algebraic theory $(\Sigma_P, E_P)$ of *convex algebras*, see [Š74, Sem73, Dob06, Dob08, Jac10], provides a presentation for the monad $\mathcal{D}$.

Another presentation of convex algebras is given by the algebraic theory with infinitely many operations denoting arbitrary (and not only binary) convex combinations $(\Sigma_{\hat{P}}, E_{\hat{P}})$ where $\Sigma_{\hat{P}}$ consists of operations $\sum_{i=1}^n p_i(\cdot)_i$ for all $n \in \mathbb{N}$ and $(p_1, \dots, p_n) \in [0, 1]^n$ such that $\sum_{i=1}^n p_i = 1$ and $E_{\hat{P}}$ is the set of the following two axioms.

$$ 
\begin{array}{ll}
\displaystyle\sum_{i=0}^{n} p_i x_i \stackrel{(P)}{=} x_j & \text{if } p_j = 1 \\[1.5em]
\displaystyle\sum_{i=0}^{n} p_i \left( \sum_{j=0}^{m} q_{i,j} x_j \right) \stackrel{(BC)}{=} \sum_{j=0}^{m} \left( \sum_{i=0}^{n} p_i q_{i,j} \right) x_j.
\end{array}
 $$

Here, $(P)$ stands for projection, and $(BC)$ for barycentre. This allows us to interchangeably use binary convex combinations or arbitrary convex combinations whenever more convenient. Moreover, we can write binary convex combinations $+_p$ for $p \in [0, 1]$ and not just $p \in (0, 1)$.

Convex algebras are known under many names: “convex modules” in [PR95], “positive convex structures” in [Dob06] (where $X$ is taken to be endowed with the discrete topology), “sets with a convex structure” in [Š74], and barycentric algebras [Sto49]. We refer to the theory of convex algebras as the algebraic theory for probability.
**Remark 3.7.** Let $\mathcal{X}$ be a $(\Sigma_{\hat{p}}, E_{\hat{p}})$-algebra. Then (for $p_n \neq 1$ and $\overline{p_n} = 1 - p_n$)

$$ \sum_{i=1}^{n} p_i x_i = \overline{p_n} \left( \sum_{j=1}^{n-1} \frac{p_j}{\overline{p_n}} x_j \right) + p_n x_n. \qquad (3.5) $$

Hence, an $n$-ary convex combination can be written as a binary convex combination using an $(n-1)$-ary convex combination.

One can also see Equation (3.5) as a definition – the classical definition of Stone [Sto49, Definition 1]. The following property, whose proof follows by induction along the lines of [Sto49, Lemma 1–Lemma 4], gives the connection:

Let $X$ be the carrier of a $(\Sigma_P, E_P)$-algebra. Define $n$-ary convex operations inductively by the projection axiom and the formula (3.5). Then $X$ becomes an algebra in $(\Sigma_{\hat{p}}, E_{\hat{p}})$.

**Presenting** $\cdot + 1$ The algebraic theory $(\Sigma_T, E_T)$ for the termination monad consists of a single constant (nullary operation symbol) $\Sigma_T = \{\star\}$ and no equations $E_T = \emptyset$. This is called the theory of *pointed sets*.

**Combining Algebraic Theories** Algebraic theories can be combined in a number of general ways: by taking their coproduct, their tensor, or by means of distributive laws (see e.g. [HPP02]). Unfortunately, these abstract constructions do not lead to a presentation for the monad we are interested in. We will thus devote the next section to show a “hand-made” presentation for this monad.

We conclude this section with a well known fact that can be easily proved, for instance using the distributive law in (3.1): given a presentation $(\Sigma, E)$ for a monad $M$, the monad $M(\cdot + 1)$ is presented by the theory $(\Sigma', E)$ where $\Sigma'$ is $\Sigma$ together with an extra constant $\star$. For instance, the subdistributions monad $\mathcal{D}(\cdot + 1)$ is presented by the theory $(\Sigma_P \cup \Sigma_T, E_P)$ of *pointed convex algebras*, also known as *positive convex algebras*. The theory $(\Sigma_N \cup \Sigma_T, E_N)$ of *pointed semilattices* provides instead a presentation for the monad $\mathcal{P}_{ne}(\cdot + 1)$. It is interesting to observe that the powerset monad $\mathcal{P}$ is presented by adding to $(\Sigma_N \cup \Sigma_T, E_N)$ the equation

$$ x \oplus \star \stackrel{(B)}{=} x $$

leading to the theory of *semilattices with bottom*. The theory of *semilattices with top* can be obtained by adding instead the following equation:

$$ x \oplus \star \stackrel{(T)}{=} \star. $$

Similar axioms can be added to the theory of pointed convex algebras $(\Sigma_P \cup \Sigma_T, E_P)$. The axiom

$$ x +_p \star \stackrel{(B_p)}{=} x $$
makes the probabilistic structure collapse, i.e., $x +_p y = x +_q y$ holds for any $p, q \in (0, 1)$:

$$ 
\begin{align*}
x +_p y &\overset{(B_p)}{=} (x +_q \star) +_p y \\
&\overset{(A_p)}{=} x +_{pq} (\star + \frac{p(1-q)}{1-pq}) y \\
&\overset{(B_p)}{=} x +_{pq} y \\
&\overset{(B_p)}{=} x +_{pq} (\star + \frac{q(1-p)}{1-pq}) y \\
&\overset{(A_p)}{=} (x +_p \star) +_q y \\
&\overset{(B_p)}{=} x +_q y
\end{align*}
$$

At the monad level, adding the axioms $(B_p)$ can be seen as the quotient of monads supp: $\mathcal{D}(\cdot + 1) \Rightarrow \mathcal{P}$ mapping each sub-distribution into its support (e.g., $(x +_p y) +_q \star$ becomes $x + y$).

On the other hand, the axiom

$$ x +_p \star \overset{(T_p)}{=} \star $$

quotients the monad $\mathcal{D}(\cdot + 1)$ into $\mathcal{D} + 1$, recall Example 3.2. Intuitively, each term of this theory is either a sum of only variables (a distribution) or an extra element $(\star)$. This axiom describes the unique functorial way of adding termination to a convex algebra, the so-called black-hole behaviour of $\star$, cf. [SW18].

## 4. ALGEBRAIC THEORY FOR NONDETERMINISM AND PROBABILITY

In this section we recall the definition of the monad $C$ for probability and nondeterminism, give its presentation via *convex semilattices*, and present examples of $C$-algebras.

### 4.1. The monad $C$ of convex subsets of distributions.
The monad $C$ origins in the field of domain theory [Mis00, J.G08, TKP09], and in the work of Varacca and Winskel [Var03, VW06]. Jacobs [Jac08] gives a detailed study of (a generalisation of) this monad.

For a set $X$, $CX$ is the set of non-empty, finitely-generated convex subsets of distributions on $X$, i.e.,

$$ CX = \{S \subseteq \mathcal{D}X \mid S \neq \emptyset, \mathrm{conv}(S) = S, S \text{ is finitely generated}\}. $$

Recall that, for a subset $S$ of a convex algebra, $\mathrm{conv}(S)$ is the convex closure of $S$, i.e., the smallest convex set that contains $S$, i.e.,

$$ \mathrm{conv}(S) = \{ \sum p_i x_i \mid p_i \in [0, 1], \sum p_i = 1, x_i \in S \}. $$

We say that a convex set $S$ is generated by its subset $B$ if $S = \mathrm{conv}(B)$. In such a case we also say that $B$ is a basis for $S$. A convex set $S$ is finitely generated if it has a finite basis.

For a function $f: X \to Y$, $Cf: CX \to CY$ is given by

$$ Cf(S) = \{ \mathcal{D}f(d) \mid d \in S \} = \overline{\mathcal{D}f(S)}. $$

The unit of $C$ is $\eta: X \to CX$ given by $\eta(x) = \{\delta_x\}$.
The multiplication of $C$, $\mu$: $CCX \to CX$ can be expressed in concrete terms as
follows [Jac08]. Given $S \in CCX$,

$$ \mu(S) = \bigcup_{\Phi \in S} \left\{ \sum_{U \in \text{supp}(\Phi)} \Phi(U) \cdot d \mid d \in U \right\}. $$

Hence, $d \in \mu(S)$ if and only if there exists $\Phi \in S$ and for all $U \in \text{supp}(\Phi)$ there exists $d_U \in U$ such that $d = \sum_{U \in \text{supp}(\Phi)} \Phi(U) \cdot d_U$.

For later use it is convenient to observe that the assignment $S \mapsto \text{conv}(S)$ gives rise to
a natural transformation [Mio14, BSS17], that we refer hereafter as

$$ \text{conv}: \mathcal{P}_{ne}\mathcal{D} \Rightarrow C \qquad (4.1) $$

The following lemma summarises the relationship between the monads $\mathcal{P}_{ne}$, $\mathcal{D}$, and $C$. Note
here that $\mathcal{P}_{ne}\mathcal{D}$ is not a monad.

**Lemma 4.1.** Consider the natural transformations depicted in the diagram on the left below.

$$ \begin{tikzcd} & C \arrow[r, "\text{conv}"] \arrow[d] \\ \mathcal{D} \arrow[r, "\eta_{\mathcal{D}}^{\mathcal{P}_{ne}}"'] & \mathcal{P}_{ne}\mathcal{D} \arrow[d, "\eta_{\mathcal{P}_{ne}}^{\mathcal{D}}"] \arrow[r] & \mathcal{P}_{ne} \end{tikzcd} $$

Then

(1) $\chi^{\mathcal{P}_{ne}} = \text{conv} \circ \mathcal{P}_{ne}\eta^{\mathcal{D}}$ is an injective monad map.

(2) $\chi^{\mathcal{D}} = \text{conv} \circ \eta_{\mathcal{D}}^{\mathcal{P}_{ne}}$ is an injective monad map.

*Proof.* Here, it is most important to notice that $\chi^{\mathcal{D}}(\varphi) = \{\varphi\}$, for any distribution $\varphi$, as singleton sets are convex, and $\chi^{\mathcal{P}_{ne}}(S) = \mathcal{D}S$. Keeping this in mind, it is not difficult to check that the diagrams needed for $\chi^{\mathcal{D}}$ and $\chi^{\mathcal{P}_{ne}}$ to be monad maps indeed commute. For the unit diagrams, we have:

$$ \chi^{\mathcal{D}} \circ \eta^{\mathcal{D}}(x) = \chi^{\mathcal{D}}(\delta_x) = \{\delta_x\} = \eta^C(x) $$

and

$$ \chi^{\mathcal{P}_{ne}} \circ \eta^{\mathcal{P}_{ne}}(x) = \chi^{\mathcal{P}_{ne}}(\{x\}) = \{\delta_x\} = \eta^C(x). $$

For the multiplication diagrams, we derive, given $\Phi \in \mathcal{D}\mathcal{D}X$,

$$ \chi^{\mathcal{D}} \circ \mu^{\mathcal{D}}(\Phi) = \chi^{\mathcal{D}} \left( \sum_{\varphi \in \mathcal{D}X} \Phi(\varphi) \cdot \varphi \right) = \left\{ \sum_{\varphi \in \mathcal{D}X} \Phi(\varphi) \cdot \varphi \right\} $$

and

$$ \begin{align*} \mu^C \circ C\chi^\mathcal{D} \circ \chi^\mathcal{D}\mathcal{D}(\Phi) &= \mu^C \circ C\chi^\mathcal{D}(\{\Phi\}) \\ &= \mu^C \left( \sum_{\varphi \in \mathcal{D}X} \Phi(\varphi) \cdot \{\varphi\} \right) \\ &= \left\{ \sum_{\varphi \in \mathcal{D}X} \Phi(\varphi) \cdot \varphi \right\}. \end{align*} $$
Given $\mathcal{S} = \{S_i \mid i \in I\}$ for $S_i \subseteq X, S_i \neq \emptyset, I \neq \emptyset$, that is $\mathcal{S} \in \mathcal{P}_{ne}\mathcal{P}_{ne}(X)$, we have

$$ \chi^{\mathcal{P}_{ne}} \circ \mu^{\mathcal{P}_{ne}}(\mathcal{S}) = \chi^{\mathcal{P}_{ne}}\left(\bigcup_{i \in I} S_i\right) = \mathcal{D}\left(\bigcup_{i \in I} S_i\right) $$

and

$$ \begin{aligned} \mu^C \circ \chi^{\mathcal{P}_{ne}} C \circ \mathcal{P}_{ne} \chi^{\mathcal{P}_{ne}}(\mathcal{S}) &= \mu^C \circ \chi^{\mathcal{P}_{ne}} C(\{\mathcal{D}S_i \mid i \in I\}) \\ &= \mu^C (\mathcal{D}\{\mathcal{D}S_i \mid i \in I\}) \\ &= \mathcal{D}\left(\bigcup_{i \in I} S_i\right) \end{aligned} $$

where the inclusion $\subseteq$ in the last equality is obvious, and the inclusion $\supseteq$ can be derived by simple grouping and normalisation, as follows. Given $d \in \mathcal{D}(\bigcup_{i \in I} S_i)$, i.e., $d = \sum_{j \in J} p_j x_j$ where $x_j \in \bigcup_{i \in I} S_i$, let $(J_i | i \in I)$ be a partition of $J$ with the property $j \in J_i \Rightarrow x_j \in S_i$, and let $p_i = \sum_{j \in J_i} p_j$. Let, moreover,

$$ d_i = \sum_{j \in J_i} \frac{p_j}{p_i} \cdot x_j $$

if $p_i \neq 0$, and $d_i = \delta_x$ for some $x \in S_i$ otherwise. Then $d = \sum_{i \in I} p_i d_i \in \mathcal{D}\{\mathcal{D}S_i \mid i \in I\}$.

Injectivity follows directly from $\chi^{\mathcal{D}}(\varphi) = \{\varphi\}$ and $\chi^{\mathcal{P}_{ne}}(S) = \mathcal{D}S$, the latter since $\mathcal{D}S = \mathcal{D}S'$ if and only if $S = S'$. $\square$

## 4.2. The presentation of C.
We now introduce the algebraic theory $(\Sigma_{NP}, E_{NP})$ of convex semilattices, that gives us the presentation of $C$ and thus provides an algebraic theory for nondeterminism and probability.

A convex semilattice $\mathbb{A}$ is an algebra $\mathbb{A} = (A, \oplus, +_p)$ with a binary operation $\oplus$ and for each $p \in (0, 1)$ a binary operation $+_p$ satisfying the axioms (A), (C), (I) of a semilattice, the axioms $(A_p), (C_p), (I_p)$ for a convex algebra, and the following distributivity axiom:

$$ (x \oplus y) +_p z \stackrel{(D)}{=} (x +_p z) \oplus (y +_p z) $$

Hence, $(\Sigma_{NP}, E_{NP})$ is given by $\Sigma_{NP} = \Sigma_N \cup \Sigma_P$ and $E_{NP} = E_N \cup E_P \cup \{(D)\}$.

In every convex semilattice there also holds a convexity law, of which we directly present the generalised version in the following lemma.

**Lemma 4.2.** Let $\mathbb{A} = (A, \oplus, +_p)$ be a convex semilattice. Then for all $n \in \mathbb{N}$, all $a_1, \dots, a_n \in \mathbb{A}$ and all $p_1, \dots, p_n \in [0, 1]$ with $\sum_{i=1}^n p_i = 1$ we have

$$ a_1 \oplus \dots \oplus a_n \oplus \sum_{i=1}^{n} p_i a_i \stackrel{(C)}{=} a_1 \oplus \dots \oplus a_n. \quad \square $$

*Proof.* For $n = 1$ the property amounts to idempotence. Assume $n > 1$ and the property holds for $n - 1$.

Below, we will write $(D)$ also for generalised distributivity as in

$$ \bigoplus_i a_i +_p \bigoplus_j b_j \stackrel{(D)}{=} \bigoplus_{i,j} (a_i +_p b_j). $$
First, we observe that

$$a_1 \oplus \dots \oplus a_n = a_1 \oplus \dots \oplus a_n \oplus \bigoplus_i (a_i + p_1 \bigoplus_{j \neq i} a_j) \quad (4.2)$$

which follows from

$$ \begin{align*} a_1 \oplus \dots \oplus a_n &\stackrel{(I_p)}{=} (a_1 \oplus \dots \oplus a_n) + p_1 (a_1 \oplus \dots \oplus a_n) \\ &\stackrel{(D)}{=} \bigoplus_{i,j} (a_i + p_1 a_j) \\ &\stackrel{(I_p, D)}{=} a_1 \oplus \dots \oplus a_n \oplus \bigoplus_i (a_i + p_1 \bigoplus_{j \neq i} a_j) \end{align*} $$

Recall that we write $\bar{p}$ for $1-p$ if $p \in [0,1]$. Furthermore, having in mind that $\sum_{i=1}^n p_i a_i = a_1 + p_1 (\sum_{i=2}^n \frac{p_i}{p_1} a_i)$ we have

$$ \begin{align*} a_1 + p_1 \left( \bigoplus_{j \neq 1} a_j \right) &\stackrel{\text{IH}}{=} a_1 + p_1 \left( \bigoplus_{j \neq 1} a_j \oplus \sum_{j \neq 1} \frac{p_j}{p_1} a_j \right) \\ &\stackrel{(D)}{=} (a_1 + p_1 \bigoplus_{j \neq 1} a_j) \oplus (a_1 + p_1 \sum_{j \neq 1} \frac{p_j}{p_1} a_j) \\ &\stackrel{\text{I}}{=} (a_1 + p_1 \bigoplus_{j \neq 1} a_j) \oplus \sum_i p_i a_i. \end{align*} $$

Using this in the second equality below, we get

$$ \begin{align*} a_1 \oplus \dots \oplus a_n \oplus \sum_{i=1}^{n} p_i a_i &\stackrel{(4.2)}{=} a_1 \oplus \dots \oplus a_n \oplus \bigoplus_{i} (a_i + p_1 \bigoplus_{j \neq i} a_j) \oplus \sum_{i=1}^{n} p_i a_i \\ &= a_1 \oplus \dots \oplus a_n \oplus \bigoplus_{i} (a_i + p_1 \bigoplus_{j \neq i} a_j) \\ &\stackrel{(4.2)}{=} a_1 \oplus \dots \oplus a_n. \quad \square \end{align*} $$

We next formulate a property that provides a way to prove that an algebraic theory is a presentation for a monad, which we will later apply in the proof that $(\Sigma_{NP}, E_{NP})$ is a presentation for $C$.

**Proposition 4.3.** Let $\mathbf{A}$ be the category of $(\Sigma, E)$-algebras with signature $\Sigma$ and equations $E$. Let $U: \mathbf{A} \to \mathbf{Sets}$ be the forgetful functor. In order to prove that $(\Sigma, E)$ is a presentation for a monad $(M, \eta, \mu)$, it suffices to:

1. For any set $X$, define $\Sigma$-operations $\Sigma_X$ on $MX$ and prove that with these operations $(MX, \Sigma_X)$ is an algebra in $\mathbf{A}$. Moreover prove that for any map $f: X \to Y$, $Mf$ is an $\mathbf{A}$-homomorphism from $(MX, \Sigma_X)$ to $(MY, \Sigma_Y)$.

2. Prove that $(MX, \Sigma_X)$ is the free algebra in $\mathbf{A}$ generated by $X$, i.e., for any algebra $\mathbb{A} = (A, \Sigma_A)$ in $\mathbf{A}$ and any map $f: X \to A$, there is a unique homomorphism $f^\# : (MX, \Sigma_X) \to \mathbb{A}$ that extends $f$, i.e., that satisfies $f = Uf^\# \circ \eta$.

3. Prove that $\mu_X = (\mathrm{id}_{MX})^\#$.
*Proof.* Assume that 1.-3. hold. We show that $M$ is presented by $(\Sigma, E)$, as explained in Remark 3.6. We provide a left adjoint to the forgetful functor such that $M$ is the monad that arises from this adjunction. We start with defining the adjunction explicitly.

Let $F: \mathbf{Sets} \to \mathbf{A}$ be the functor defined on objects as $FX = (MX, \Sigma_X)$. Hence, $UFX = MX$. On arrows $f: X \to Y$, we set $Ff = (\eta \circ f)^\#$.

Then $F$ is a left adjoint of the forgetful functor $U$, and the adjunction is given by the bijective correspondence $(f: X \to UA) \mapsto (f^\# : FX \to A)$. This is injective since: $f^\# = g^\# \Rightarrow f = Uf^\# \circ \eta = Ug^\# \circ \eta = g$. It is surjective since: for a homomorphism $h^*: FX \to A$, we consider $h = Uh^* \circ \eta$ and since $h^\# = h^*$ is the unique homomorphism such that $h = Uh^\# \circ \eta$, we get that $h^\# = h^*$.

Next, we see that $UfF = Mf$ as a consequence of naturality of $\eta$. Namely, we have that $Ff = (\eta \circ f)^\#$ is the unique homomorphism with the property $UfF \circ \eta = \eta \circ f$. Hence, using 1., since $Mf \circ \eta = \eta \circ f$ by naturality of $\eta$, we get $UfF = Mf$.

Let $(T, \bar{\eta}, \bar{\mu})$ be the monad of this adjunction. This means that, see e.g. [Mac71, VI.1, IV.1], $T = UF$, $(\bar{\eta})^\# = id_{FX}$ and $\bar{\mu} = U\varepsilon F$ where $\varepsilon_A = (id_{UA})^\#$ is the counit of the adjunction, and hence $\bar{\mu}_X = (id_{MX})^\#$. We next show that $\eta^\# = id_{FX}$ which implies $\bar{\eta} = \eta$. All we need to observe is that $U\bar{id}_{FX} \circ \eta = id_{UFX} \circ \eta = \eta$ and since $\eta^\#$ is the unique homomorphism with $U\eta^\# \circ \eta = \eta$ and $id_{FX}$ is a homomorphism from $FX$ to itself, we get $\eta^\# = id_{FX}$. Finally, item 3. proves that $\bar{\mu} = \mu$. $\square$

For $p \in [0, 1]$ we set $\bar{p} = 1 - p$. Let $X$ be an arbitrary set. We define $\Sigma_{NP}$-operations on $CX$ by

$$S_1 \oplus S_2 = \mathrm{conv}(S_1 \cup S_2)$$

and for $p \in (0, 1)$

$$S_1 +_p S_2 = \{\varphi \mid \varphi = p\varphi_1 + \bar{p}\varphi_2 \text{ for some } \varphi_1 \in S_1, \varphi_2 \in S_2\}$$

where $p\varphi_1 + \bar{p}\varphi_2 = \varphi_1 +_p \varphi_2$ is the binary convex combination of $\varphi_1$ and $\varphi_2$ in $\mathcal{D}X$, defined point-wise. Note that $S_1 +_p S_2$ is the Minkowski sum of two convex sets. If convenient, we may sometimes also write, as usual, $pS_1 + \bar{p}S_2$ for the Minkowski sum $S_1 +_p S_2$.

The proof of the presentation follows the structure of Proposition 4.3 via the following three lemmas.

**Lemma 4.4.** With the above defined operations $(CX, \oplus, +_p)$ is a convex semilattice, for any set $X$. Moreover, for a map $f: X \to Y$, the map $Cf: CX \to CY$ is a convex semilattice homomorphism from $(CX, \oplus, +_p)$ to $(CY, \oplus, +_p)$. $\square$

**Lemma 4.5.** The convex semilattice $(CX, \oplus, +_p)$ is the free convex semilattice generated by $\eta(X)$. $\square$

**Lemma 4.6.** The multiplication $\mu$ of the monad $C$ satisfies $\mu = (id_{CX})^\#$. $\square$

All detailed proofs are in Section 4.3, where we also list some additional helpful properties. Now all ingredients are in place and we get the presentation for $C$ directly from Proposition 4.3.

**Theorem 4.7.** The theory for nondeterminism and probability $(\Sigma_{NP}, E_{NP})$, i.e., the theory of convex semilattices, is a presentation for the monad $C$. $\square$

**Remark 4.8.** Theorem 4.7 is to some extent known<fnref n="3" /> but we could not find a proof of it in the literature. In [Var03, VW06] a monad for probability and nondeterminism is given

<footnote n="3">³Personal communication with Gordon Plotkin.</footnote>
starting from a similar algebraic theory (with somewhat different basic algebraic structure). The observation that the distributive law (D) gives rise to convex subsets was known at least since [MOW03]. Indeed, all the axioms in $E_{NP}$ already appear in [MOW03] that additionally contains the axiom (B) and $(T_p)$ for dealing with termination. Nevertheless, in [MOW03] these axioms are not related to any particular monad. There is also another possible way of combining probability with nondeterminism, by distributing $\oplus$ over $+_p$ (see e.g. [KP17, DPS18]).

**Remark 4.9.** Having the presentation enables us to identify and interchangeably use convex subsets of distributions and terms in $\Sigma_{NP}$ modulo equations in $E_{NP}$. This is particularly useful in examples and our further developments. Note that in the syntactic view $\eta(x)$ is identified with the term $x$.

The presentation is a valuable tool in many situations where reasoning with algebraic theories is more convenient than reasoning with monads. For instance, it is much easier to check whether a certain algebra is a $(\Sigma_{NP}, E_{NP})$-model, than to check that it is an algebra for the monad $C$. We illustrate this with three $(\Sigma_{NP}, E_{NP})$ models that play a key role in our further results and exposition.

**The max convex semilattice** $\text{Max} = ([0, 1], \max, +_p)$ is a $(\Sigma_{NP}, E_{NP})$-algebra when taking $\oplus$ to be max: $[0, 1] \times [0, 1] \to [0, 1]$ and $+_p$ the standard convex combination $+_p: [0, 1] \times [0, 1] \to [0, 1]$ with $x+_p y = p \cdot x + \bar{p} \cdot y$ for $x, y \in [0, 1]$. To check that this is a $(\Sigma_{NP}, E_{NP})$ model, it is enough to prove that max satisfies the axioms in $E_N$, that $+_p$ satisfies the axioms in $E_P$, and that they satisfy the axiom (D), namely that $\max(x, y)+_p z = \max(x+_p z, y+_p z)$.

**The min convex semilattice** $\text{Min} = ([0, 1], \min, +_p)$ is obtained similarly by taking $\oplus$ to be min: $[0, 1] \times [0, 1] \to [0, 1]$ rather than max, and gives another example of a $(\Sigma_{NP}, E_{NP})$-algebra. It is indeed very simple to check that $([0, 1], \min)$ forms a semilattice and that the distributivity law holds.

**The min-max interval convex semilattice** We consider the algebraic structure $M_J = (J, \min, \max, +_p^j)$ for $J$ the set of intervals on $[0, 1]$, i.e.,

$$J = \{[x, y] \mid x, y \in [0, 1] \text{ and } x \le y\}.$$

For $[x_1, y_1], [x_2, y_2] \in J$, we define $\min-max: J \times J \to J$ as

$$\min-max([x_1, y_1], [x_2, y_2]) = [\min(x_1, x_2), \max(y_1, y_2)]$$

and $+_p^j: J \times J \to J$ by

$$[x_1, y_1] +_p^j [x_2, y_2] = [x_1 +_p x_2, y_1 +_p y_2].$$

The fact that this is a model for $(\Sigma_{NP}, E_{NP})$ follows easily from the fact that $\text{Max}$ and $\text{Min}$ are models for $(\Sigma_{NP}, E_{NP})$.

**Remark 4.10.** The fact that $\text{Max}$ and $\text{Min}$ are $C$-algebras on $[0, 1]$ was already proven in [vHHOS18], without an algebraic presentation. Having the algebraic presentation significantly simplifies the proofs.
### 4.3. Auxiliary Lemmas for the Proof of the Presentation of C.
Before we proceed with the proof of the presentation, we recall several properties that are known or immediate to check, but very helpful in our further proofs.

**Lemma 4.11.** Let $\mathbb{A}$ and $\mathbb{B}$ be two convex algebras, and $f: \mathbb{A} \to \mathbb{B}$ a convex homomorphism. Then for all $X \in \mathcal{P}_u A$, for $\mathcal{P}_u$ being the unrestricted (not necessarily finite) powerset, $\mathrm{conv}_{\mathbb{B}} \bar{f}(X) = \bar{f}(\mathrm{conv}_{\mathbb{A}} X)$. In particular, if $X$ is convex then also $\bar{f}(X)$ is convex.

*Proof.* For $\subseteq$, for an arbitrary $pf(x) + \bar{p}f(y) \in \mathrm{conv}_{\mathbb{B}} \bar{f}(X)$ with $x, y \in X$, we have

$$pf(x) + \bar{p}f(y) \stackrel{(*)}{=} f(px + \bar{p}y) \in \bar{f}(\mathrm{conv}_{\mathbb{A}} X)$$

where the equality marked by (*) holds by the assumption that $f$ is a convex homomorphism. For $\supseteq$, consider $f(a) \in \bar{f}(\mathrm{conv}_{\mathbb{A}} X)$. Then $a = px + \bar{p}y$ for some $x, y \in X$. Since $f$ is convex, $f(a) = pf(x) + \bar{p}f(y)$ and $f(x), f(y) \in \bar{f}(X)$. Hence $f(a) \in \mathrm{conv}_{\mathbb{B}} \bar{f}(X)$. $\square$

**Lemma 4.12.** Let $\mathbb{A}$ and $\mathbb{B}$ be two convex algebras, and $f: \mathbb{A} \to \mathbb{B}$ a convex homomorphism. Then the image map $\bar{f} = \mathcal{P}_u f: \mathcal{P}_u A \to \mathcal{P}_u B$, for $\mathcal{P}_u$ being the unrestricted (not necessarily finite) powerset, is a convex map, i.e. if $S = X +_p Y$ for $X \in \mathcal{P}_u A, Y \in \mathcal{P}_u B$, then $\bar{f}(S) = \bar{f}(X) +_p \bar{f}(Y)$.

*Proof.* Let $S = X +_p Y$ for $X \in \mathcal{P}_u A, Y \in \mathcal{P}_u B$. Then

$$\begin{align*}
\bar{f}(S) &= \{f(s) \mid s \in S\} \\
&= \{f(px + \bar{p}y) \mid x \in X, y \in Y\} \\
&\stackrel{(*)}{=} \{pf(x) + \bar{p}f(y) \mid x \in X, y \in Y\} \\
&= \bar{p}\bar{f}(X) + \bar{p}\bar{f}(Y).
\end{align*}$$

and here, again, (*) holds since $f$ is convex. $\square$

**Lemma 4.13.** Let $X$ be a set and let $S \in \mathcal{P}_u CX$ be a convex set with respect to Minkowski sum. Then $\bigcup S \in CX$.

*Proof.* Let $S = \{S_i \mid i \in I\}$. Let $\Phi, \Psi \in \bigcup S$. Then there exist $i, j \in I$ with $\Phi \in S_i$ and $\Psi \in S_j$. We have $p\Phi + \bar{p}\Psi \in pS_i + \bar{p}S_j \in S$ as $S$ is convex. $\square$

We can now prove Lemmas 4.4, 4.5, and 4.6 announced in the previous section, from which the presentation of C follows.

*Proof of Lemma 4.4.* We want to prove the following: $(CX, \oplus, +_p)$ is a convex semilattice, for any set $X$. Moreover, for a map $f: X \to Y$, the map $Cf: CX \to CY$ is a convex semilattice homomorphism from $(CX, \oplus, +_p)$ to $(CY, \oplus, +_p)$.

In any convex algebra $\mathbb{A}$ for $S, T \subseteq A$ we have

$$\mathrm{conv}(\mathrm{conv}(S) \cup T) = \mathrm{conv}(S \cup T).$$

As a consequence, using the associativity of union, we get that the axiom (A) holds. For $S_1, S_2, S_3 \in CX$:

$$\begin{align*}
S_1 \oplus (S_2 \oplus S_3) &= \mathrm{conv}(S_1 \cup \mathrm{conv}(S_2 \cup S_3)) \\
&= \mathrm{conv}(S_1 \cup (S_2 \cup S_3)) \\
&= \mathrm{conv}((S_1 \cup S_2) \cup S_3) \\
&= \mathrm{conv}(\mathrm{conv}(S_1 \cup S_2) \cup S_3) \\
&= (S_1 \oplus S_2) \oplus S_3.
\end{align*}$$
Commutativity and idempotence hold due to commutativity and idempotence of union.

Defining convex operations on $CX$ using Minkowski sum, see [BSS17], leads to a convex algebra, i.e., $(A_p), (C_p), (I_p)$ hold.

The axiom (D) holds as:

$$ 
\begin{aligned}
(S_1 \oplus S_2) +_p S_3 \\
&= p \operatorname{conv}(S_1 \cup S_2) + \bar{p} S_3 \\
&= \{pqd_1 + p\bar{q}d_2 + \bar{p}d_3 \mid q \in [0, 1], d_i \in S_i\} \\
&= \operatorname{conv}((pS_1 + \bar{p}S_3) \cup (pS_2 + \bar{p}S_3)).
\end{aligned}
$$

Finally, $Cf$ is a homomorphism from $(CX, \oplus, +_p)$ to $(CY, \oplus, +_p)$ as

$$ 
\begin{aligned}
Cf(S_1 \oplus S_2) &= \overline{\mathcal{D}f}(S_1 \oplus S_2) \\
&\stackrel{(a)}{=} \operatorname{conv}(\overline{\mathcal{D}f}(S_1 \cup S_2)) \\
&= \operatorname{conv}(\overline{\mathcal{D}f}(S_1) \cup \overline{\mathcal{D}f}(S_2)) \\
&= \overline{\mathcal{D}f}(S_1) \oplus \overline{\mathcal{D}f}(S_2) \\
&= Cf(S_1) \oplus Cf(S_2)
\end{aligned}
$$

where the equality marked by (a) holds by Lemma 4.11. Similarly

$$ 
\begin{aligned}
Cf(S_1 +_p S_2) &= \overline{\mathcal{D}f}(S_1 +_p S_2) \\
&\stackrel{(b)}{=} \overline{\mathcal{D}f}(S_1) +_p \overline{\mathcal{D}f}(S_2) \\
&= Cf(S_1) +_p Cf(S_2).
\end{aligned}
$$

where the equality marked by (b) holds by Lemma 4.12. $\square$

*Proof of Lemma 4.5.* We want to prove the following: The convex semilattice $(CX, \oplus, +_p)$ is the free convex semilattice generated by $\eta(X)$.

We need to show that for any map $f: X \to A$ for a convex semilattice $\mathbb{A} = (A, \oplus, +_p)$, there is a unique convex semilattice homomorphism $f^{\#}: (CX, \oplus, +_p) \to \mathbb{A}$ such that $Uf^{\#} \circ \eta = f$. So, let $\mathbb{A} = (A, \oplus, +_p)$ be a convex semilattice, and let $f: X \to A$ be a map. We use the same notation for the operations in $A$ and in $CX$ for simplicity.

Note that, since any convex semilattice is a convex algebra, there is a unique convex homomorphism $f_{\mathbb{D}}^{\#}: \mathcal{D}X \to (A, +_p)$, as $\mathcal{D}X$ is the free convex algebra generated by $\eta_{\mathbb{D}}(X)$. Hence, $Uf_{\mathbb{D}}^{\#} \circ \eta_{\mathbb{D}} = f$.

Now, given a convex set $S = \operatorname{conv}\{d_1, \dots, d_n\} \in CX$ we put

$$ f^{\#}(S) = f_{\mathbb{D}}^{\#}(d_1) \oplus f_{\mathbb{D}}^{\#}(d_2) \oplus \dots \oplus f_{\mathbb{D}}^{\#}(d_n). $$

We first prove that $f^{\#}$ is well defined, which is the most important step. We show that whenever

$$ \operatorname{conv}\{d_1, \dots, d_n\} = \operatorname{conv}\{e_1, \dots, e_m\} \qquad (4.3) $$

then

$$ f_{\mathbb{D}}^{\#}(d_1) \oplus \dots \oplus f_{\mathbb{D}}^{\#}(d_n) = f_{\mathbb{D}}^{\#}(e_1) \oplus \dots \oplus f_{\mathbb{D}}^{\#}(e_m). $$

Clearly, if Equation (4.3) holds, then for all $i \in \{1, \dots, n\}$, $d_i \in \operatorname{conv}\{e_1, \dots, e_m\}$ and for all $j \in \{1, \dots, m\}$, $e_j \in \operatorname{conv}\{d_1, \dots, d_n\}$. Hence,

$$ \operatorname{conv}\{d_1, \dots, d_n, e_1, \dots, e_m\} = \operatorname{conv}\{d_1, \dots, d_n\} = \operatorname{conv}\{e_1, \dots, e_n\}. $$
If we can prove that whenever $e \in \text{conv}\{d_1, \dots, d_n\}$ then

$$f_{\mathcal{D}}^{\#}(d_1) \oplus \dots \oplus f_{\mathcal{D}}^{\#}(d_n) \oplus f_{\mathcal{D}}^{\#}(e) = f_{\mathcal{D}}^{\#}(d_1) \oplus \dots \oplus f_{\mathcal{D}}^{\#}(d_n),$$

we would be done with well defined-ness as then

$$\begin{align*}
f_{\mathcal{D}}^{\#}(d_1) \oplus \dots \oplus f_{\mathcal{D}}^{\#}(d_n) \\
&= f_{\mathcal{D}}^{\#}(d_1) \oplus \dots \oplus f_{\mathcal{D}}^{\#}(d_n) \oplus f_{\mathcal{D}}^{\#}(e_1) \oplus \dots \oplus f_{\mathcal{D}}^{\#}(e_m) \\
&= f_{\mathcal{D}}^{\#}(e_1) \oplus \dots \oplus f_{\mathcal{D}}^{\#}(e_m).
\end{align*}$$

So, let $e \in \text{conv}\{d_1, \dots, d_n\}$. Then $e = \sum_i p_i d_i$ and since $f_{\mathcal{D}}^{\#}$ is a convex algebra homomorphism, $f_{\mathcal{D}}^{\#}(e) = \sum_i p_i f_{\mathcal{D}}^{\#}(d_i)$. Now, by the convexity law, Lemma 4.2, we have

$$\begin{align*}
f_{\mathcal{D}}^{\#}(d_1) \oplus \dots \oplus f_{\mathcal{D}}^{\#}(d_n) \oplus f_{\mathcal{D}}^{\#}(e) &= f_{\mathcal{D}}^{\#}(d_1) \oplus \dots \oplus f_{\mathcal{D}}^{\#}(d_n) \oplus \sum_i p_i f_{\mathcal{D}}^{\#}(d_i) \\
&= f_{\mathcal{D}}^{\#}(d_1) \oplus \dots \oplus f_{\mathcal{D}}^{\#}(d_n).
\end{align*}$$

It remains to show that $f^{\#}$ is a homomorphism and that it is uniquely extending $f$ on $\eta(X)$. Let $S, T \in \mathcal{C}X$. Let $S = \text{conv}\{d_1, \dots, d_n\}, T = \text{conv}\{e_1, \dots, e_m\}$.

Then $S \oplus T = \text{conv}(S \cup T) = \text{conv}\{d_1, \dots, d_n, e_1, \dots, e_m\}$ and we get

$$f^{\#}(S \oplus T) = f_{\mathcal{D}}^{\#}(d_1) \oplus \dots \oplus f_{\mathcal{D}}^{\#}(d_n) \oplus f_{\mathcal{D}}^{\#}(e_1) \oplus \dots \oplus f_{\mathcal{D}}^{\#}(e_m) = f^{\#}(S) \oplus f^{\#}(T).$$

Next, we first notice that $S +_p T = \text{conv}\{pd_i + \bar{p}e_j \mid i \in \{1, \dots, n\}, j \in \{1, \dots, m\}\}$. For $\supseteq$, we see that

$$\sum_{i,j} q_{i,j}(pd_i + \bar{p}e_j) = p \sum_{i,j} q_{i,j}d_i + \bar{p} \sum_{i,j} q_{i,j}e_j \in S +_p T.$$

For $\subseteq$, take $pd + \bar{p}e \in S +_p T$. So, $d = \sum_i q_i d_i$ and $e = \sum_j r_j e_j$ and we have

$$\begin{align*}
pd + \bar{p}e &= p \sum_{i} q_i d_i + \bar{p} \sum_{j} r_j e_j \\
&= p \sum_{i} q_i \left( \sum_{j} r_j \right) d_i + \bar{p} \sum_{j} r_j \left( \sum_{i} q_i \right) e_j \\
&= \sum_{i,j} q_i r_j (pd_i + \bar{p}e_j).
\end{align*}$$

Now

$$\begin{align*}
f^{\#}(S +_p T) &= \bigoplus_{i,j} f_{\mathcal{D}}^{\#}(pd_i + \bar{p}e_j) \\
&= \bigoplus_{i,j} pf_{\mathcal{D}}^{\#}(d_i) + \bar{p}f_{\mathcal{D}}^{\#}(e_j) \\
&= \bigoplus_{i,j} f_{\mathcal{D}}^{\#}(d_i) +_p f_{\mathcal{D}}^{\#}(e_j) \\
&\stackrel{(D)}{=} (f_{\mathcal{D}}^{\#}(d_1) \oplus \dots \oplus f_{\mathcal{D}}^{\#}(d_n)) +_p (f_{\mathcal{D}}^{\#}(e_1) \oplus \dots \oplus f_{\mathcal{D}}^{\#}(e_m)) \\
&= f^{\#}(S) +_p f^{\#}(T).
\end{align*}$$
Finally, assume $f^*: (CX, \oplus, +_p) \to A$ is another homomorphism that extends $f$ on $\eta(X)$, i.e., such that $Uf^* \circ \eta = f$. Then $f^*(\{\delta_x\}) = f^*(\{\delta_x\}) = f(x)$. Since both $f^\#$ and $f^*$ are convex homomorphisms, and $\{\sum_i p_i x_i\} = \sum_i p_i \{\delta_{x_i}\}$, we get

$$f^*(\{\sum_i p_i x_i\}) = \sum_i p_i f^*(\{\delta_{x_i}\}) = \sum_i p_i f^*(\{\delta_{x_i}\}) = f^*(\{\sum_i p_i x_i\}).$$

Further on, for $S = \text{conv}\{d_1, \dots, d_n\}$ we have $S = \{d_1\} \oplus \dots \oplus \{d_n\}$ and hence $f^*(S) = f^*(\{d_1\}) \oplus \dots \oplus f^*(\{d_n\}) = f^*(\{d_1\}) \oplus \dots \oplus f^*(\{d_n\}) = f^*(S)$ shows that $f^* = f^\#$ and completes the proof. $\square$

The final missing property for the presentation, Lemma 4.6, is an easy consequence of the next property that clarifies the definition of $f^\#$.

**Lemma 4.14.** Let $X$ be a set and $f: X \to CY$ a map. Then for all $S$ in $CX$

$$f^\#(S) = \bigcup \overline{f_D^\#}(S) = \bigcup_{\Phi \in S} \sum_{u \in \text{supp}(\Phi)} \Phi(u) \cdot f(u).$$

*Proof.* The first task is to prove that $f^\#(S) = \bigcup \overline{f_D^\#}(S)$. Before we proceed, let's recall all the types. We have $f: X \to CY$ (and $CY$ is the carrier of a convex semilattice), so $f^\#: CX \to CY$. Also, $f_D^\#: DX \to CY$ and hence $\overline{f_D^\#}: P_u DX \to P_u CY$ for $P_u$ denoting the unrestricted (and not just finite) powerset. Finally, here $\cup: P_u P_u DY \to P_u DY$. Clearly, $CZ \subseteq P_u DZ$ for any set $Z$.

Now, since $S$ is convex, by Lemma 4.11 also $\overline{f_D^\#}(S)$ is convex. Each element of $\overline{f_D^\#}(S)$ is of the form $f_D^\#(\Phi)$ for $\Phi \in S$ and hence it is in $CY$, i.e., is convex. By Lemma 4.13, we get that $\bigcup \overline{f_D^\#}(S)$ is convex.

Let $\Psi_1, \dots, \Psi_n \in DX$ be such that $S = \text{conv}\{\Psi_1, \dots, \Psi_n\}$. Clearly, $\Psi_1, \dots, \Psi_n \in S$. Now, we have

$$\{f_D^\#(\Psi_i) | i = 1, \dots, n\} \subseteq \{f_D^\#(\Phi) | \Phi \in S\}$$

and hence

$$\bigcup \{f_D^\#(\Psi_i) | i = 1, \dots, n\} \subseteq \bigcup \{f_D^\#(\Phi) | \Phi \in S\} = \bigcup \overline{f_D^\#}(S)$$

and since the set on the right hand side is convex, as we noted above,

$$f^\#(S) = \bigoplus_i f_D^\#(\Psi_i) = \text{conv} \bigcup_i \{f_D^\#(\Psi_i) | i = 1, \dots, n\} \subseteq \bigcup_i \{f_D^\#(\Phi) | \Phi \in S\},$$

where the first equality is simply the definition of $f^\#$.

For the other inclusion, let $\Phi \in S$. Then $S = \text{conv}\{\Psi_1, \dots, \Psi_n, \Phi\}$ and

$$f^\#(S) = \text{conv} \bigcup_i \{f_D^\#(\Psi_i), \dots, f_D^\#(\Psi_n), f_D^\#(\Phi)\}$$

by the definition of $f^\#$. Therefore, $f_D^\#(\Phi) \subseteq f^\#(S)$ and since $\Phi$ was arbitrary,

$$\bigcup \{f_D^\#(\Phi) | \Phi \in S\} \subseteq f^\#(S).$$
This proves the first equality of our statement. For the second equality, note that

$$ 
\begin{align*}
f^{\#}(S) &= \bigcup \{f_{\mathcal{D}}^{\#}(\Phi) \mid \Phi \in S\} \\
&\stackrel{(*)}{=} \bigcup \left\{ \sum_{u \in \text{supp}(\Phi)} \Phi(u) \cdot f(u) \mid \Phi \in S \right\} \\
&= \bigcup_{\Phi \in S} \sum_{u \in \text{supp}(\Phi)} \Phi(u) \cdot f(u)
\end{align*}
$$

where the equality (*) holds as $f_{\mathcal{D}}^{\#}$ is convex.

<figure><img src="image_16.png" /></figure>

*Proof of Lemma 4.6.* Using Lemma 4.14, we immediately get

$$ (id_{CX})^{\#}(S) = \bigcup_{\Phi \in S} \sum_{A \in \text{supp}(\Phi)} \Phi(A) \cdot A = \mu_X(S). \quad \square $$

## 5. ADDING TERMINATION

So far, we have provided a presentation for the monad $C$ which combines probability and nondeterminism. In order to properly model NPLTS, we need a last ingredient: termination. As discussed in Section 3, termination is given by the monad $\cdot + 1$ which can always be safely combined with any monad. Following the discussion at the end of Section 3, the theory $\mathcal{PCS} = (\Sigma_{NP} \cup \Sigma_T, E_{NP})$ presents the monad $C(\cdot + 1)$ which is the monad of finitely generated non empty convex sets of *subdistributions*. We call this theory $\mathcal{PCS}$ since algebras for this theory are *pointed convex semilattices*, namely convex semilattices with a pointed element denoted by $\star$.

Like for the monad $\mathcal{P}_{ne}$, there exist more than one interesting way of combining $C$ with $\cdot + 1$. Rather than pointed convex semilattices, one can consider *convex semilattices with bottom*, namely algebras for the theory $\mathcal{CSB} = (\Sigma_{NP} \cup \Sigma_T, E_{NP} \cup \{(B)\})$ obtained by adding $(B)$ to $\mathcal{PCS}$. Otherwise, one can add the axiom $(T)$ and obtain the theory $\mathcal{CSJ} = (\Sigma_{NP} \cup \Sigma_T, E_{NP} \cup \{(T)\})$ of *convex semilattices with top*. We denote by $T_{\mathcal{CSB}}$ and $T_{\mathcal{CSJ}}$ the corresponding monads.

As we will illustrate in Section 6, particularly relevant for defining trace semantics is the free algebra $\mu: MM\{\bullet\} \to M\{\bullet\}$ generated by a singleton $\{\bullet\}$. In the next three propositions we respectively identify these algebras for the monad $T_{\mathcal{PCS}}$ (that is, $C(\cdot + 1)$), the monad $T_{\mathcal{CSB}}$, and the monad $T_{\mathcal{CSJ}}$ in concrete terms.

**Proposition 5.1.** $M_{\mathcal{J},[0,0]} = (\mathcal{J}, \text{min-max}, +_p^j, [0, 0])$ is the free pointed convex semilattice generated by a singleton set $1 = \{\bullet\}$.

*Proof.* Recall that $M_{\mathcal{J}} = (\mathcal{J}, \text{min-max}, +_p^j)$ is the convex semilattice of intervals from Section 4. Then, by interpreting the pointed element $\star$ as the interval $[0, 0]$ we have that $M_{\mathcal{J},[0,0]}$ is a pointed convex semilattice.

Let $2 = \{\bullet, \star\}$. Note that the carrier of the free pointed semilattice generated by $\{\bullet\}$ is $C(1+1) = C(2)$. Recall that $(C(2), \oplus, +_p)$, where $\oplus$ is the convex union and $+_p$ is the Minkowski sum, is the free convex semilattice generated by 2.

We next show that $(C(2), \oplus, +_p)$ is isomorphic to $M_{\mathcal{J}}$. Indeed $\mathcal{D}(2)$ is isomorphic to $[0, 1]$; the real number 0 corresponds to $\delta_{\star}$, 1 to $\delta_{\bullet}$ and $p \in (0, 1)$ to $\bullet +_p \star$. Furthermore, the
non-empty finitely-generated convex subsets of $[0, 1]$ are the closed intervals. To conclude, it suffices to see that $\min-\max$ is $\oplus$ on $\mathcal{J}$ and $+_{p}^{\mathcal{J}}$ is the Minkowski sum. $\square$

**Proposition 5.2.** $\mathrm{Max}_B = ([0, 1], \max, +_p, 0)$ is the free convex semilattice with bottom generated by $1 = \{\bullet\}$. $\square$

*Proof.* By Proposition 5.1, we know that $C(2)$ is isomorphic to $\mathcal{J}$. We show that $M_{\mathcal{J},[0,0]}$ modulo the axiom (B) is isomorphic to $\mathrm{Max}_B$. We have

$$ \min-\max([x, y], [0, 0]) \stackrel{(B)}{=} [x, y], $$

for $[x, y] \in \mathcal{J}$. From

$$ [0, y] = \min-\max([x, y], [0, 0]) = [x, y], $$

we derive that $[x_1, y] = [x_2, y]$ for any $x_1, x_2, y$. Hence, we define the isomorphism $[x, y] \mapsto y$ mapping any interval $[x, y]$ to its upper bound $y$.

The interval $[0, 0]$ is mapped to the bottom element 0, and the operations are such that:

$$ \begin{aligned} \min-\max([x_1, y_1], [x_2, y_2]) &= \min-\max([0, y_1], [0, y_2]) \\ &= [0, \max(y_1, y_2)] \end{aligned} $$

hence $\min-\max([x_1, y_1], [x_2, y_2]) \mapsto \max(y_1, y_2)$ and

$$ [x_1, y_1] +_p [x_2, y_2] = [0, y_1] +_p [0, y_2] = [0, y_1 +_p y_2] \mapsto y_1 +_p y_2. \quad \square $$

**Proposition 5.3.** $\mathrm{Min}_T = ([0, 1], \min, +_p, 0)$ is the free convex semilattice with top generated by $1 = \{\bullet\}$. $\square$

*Proof.* We show that $M_{\mathcal{J},[0,0]}$ modulo the (T) axiom

$$ \min-\max([x, y], [0, 0]) \stackrel{(T)}{=} [0, 0] $$

is isomorphic to $\mathrm{Min}_T$. First, we derive $[x, y_1] = [x, y_2]$ for any $x, y_1, y_2$ as follows. For $x = 1$ the property trivially holds. For $x = 0$ we have

$$ [0, y_1] = \min-\max([x, y_1], [0, 0]) \stackrel{(T)}{=} [0, 0] \stackrel{(T)}{=} \min-\max([x, y_2], [0, 0]) = [0, y_2] \quad (5.1) $$

Finally, for $x \in (0, 1)$ and $y_1, y_2 \ge x$ we derive

$$ [x, y_1] = [1, 1] +_x [0, \frac{y_1 - x}{1 - x}] \stackrel{(5.1)}{=} [1, 1] +_x [0, \frac{y_2 - x}{1 - x}] = [x, y_2]. $$

Hence, we can now map every interval $[x, y]$ to its lower bound $x$. Then $[0, 0]$ is mapped to the top element 0, and

$$ \begin{aligned} \min-\max([x_1, y_1], [x_2, y_2]) &= [\min(x_1, x_2), \max(y_1, y_2)] \mapsto \min(x_1, x_2) \\ [x_1, y_1] +_p [x_2, y_2] &= [x_1 +_p x_2, y_1 +_p y_2] \mapsto x_1 +_p x_2. \quad \square \end{aligned} $$

At this point the reader may wonder what happens when one considers the axioms $(B_p)$ and $(T_p)$ in place of $(B)$ and $(T)$. We have already shown at the end of Section 3.4, that the axiom $(B_p)$ makes the probabilistic structure collapse. When focussing on the free algebra generated by $\{\bullet\}$, also quotienting by $(T_p)$ is not really interesting: one can show by induction on the terms in $T_{\Sigma_{NP} \cup \Sigma_T}(\{\bullet\})$ that every term is equal via $E_{NP} \cup \{(T_p)\}$ to either $\bullet$ or $\star$ or $\bullet \oplus \star$.

So, we have found three interesting ways of combining termination with probability and nondeterminism. Table 2 summarises these theories, their monads, and their algebras.
## 6. COALGEBRAS AND DETERMINISATION

In this section, we briefly introduce coalgebra (Section 6.1) and the generalised determination [SBBR10] construction (Section 6.2), as well as several examples of transitions systems and automata featuring either nondeterministic or probabilistic behaviour. We present some simple facts and a novel general result (Section 6.3) that will be useful in Section 7 to prove some key properties for systems featuring –at the same time– nondeterminism and probability. At the end of this section (Section 6.4), we provide a general notion of trace semantics for transition systems and we illustrate some important examples.

**6.1. Coalgebra.** The theory of coalgebra provides an abstract framework for state-based transition systems and automata. A coalgebra for a functor $F$ in **Sets** (also called $F$-coalgebra) is a pair $(S, c)$ of a state space $S$ and a function $c: S \to FS$ where $F: \mathbf{Sets} \to \mathbf{Sets}$ specifies the type of transitions. Sometimes we say the coalgebra $c: S \to FS$, meaning the coalgebra $(S, c)$.

A coalgebra homomorphism from a coalgebra $(S, c)$ to a coalgebra $(T, d)$ is a function $h: S \to T$ that satisfies $d \circ h = Fh \circ c$. Coalgebras for a functor $F$ and their coalgebra homomorphisms form a category, denoted by Coalg $(F)$.

The final object in Coalg $(F)$, when it exists, is the final $F$-coalgebra. We write $\zeta: Z \stackrel{\sim}{\to} FZ$ for the final $F$-coalgebra. For every coalgebra $c: S \to FS$, there is a unique homomorphism $\llbracket \cdot \rrbracket_c$ to the final one, the final coalgebra map, making the diagram below commute:

$$ \begin{array}{ccc} S & \multicolumn{2}{c}{\exists! \llbracket \cdot \rrbracket_c} \\[-1.5ex] c \downarrow & & \downarrow \zeta \\ FS & \multicolumn{2}{c}{\llbracket s \rrbracket_c = \llbracket t \rrbracket_c} \end{array} $$

The final coalgebra semantics $\sim$ is the kernel of the final coalgebra map, i.e., two states $s$ and $t$ are equivalent in the final coalgebra semantics iff $\llbracket s \rrbracket_c = \llbracket t \rrbracket_c$.

Even without a final coalgebra, coalgebras over a concrete category are equipped with a generic behavioural equivalence. Let $(S, c)$ be an $F$-coalgebra on **Sets**. An equivalence relation $R \subseteq S \times S$ is a kernel bisimulation (synonymously, a cocongruence) [Sta11, Kur00, Wol00] if it is the kernel of a homomorphism, i.e., $R = \ker h = \{(s, t) \in S \times S \mid h(s) = h(t)\}$ for some coalgebra homomorphism $h: (S, c) \to (T, d)$ to some $F$-coalgebra $(T, d)$. Two states $s, t$ of a coalgebra are *behaviourally equivalent* (notation: $s \approx t$) iff there is a kernel bisimulation $R$ with $(s, t) \in R$. If a final coalgebra exists, then the behavioural equivalence and the final coalgebra semantics coincide, i.e., $\approx = \sim$.

The following are well-known examples of $F$-coalgebras that will be useful later on:

(1) Labelled transition systems, LTS, are coalgebras for the functor $F = (\mathcal{P}(\cdot))^A$. Behavioural equivalence coincides with strong bisimilarity.

(2) Nondeterministic automata, NA, are coalgebras for $F = 2 \times (\mathcal{P}(\cdot))^A$ where $2 = \{0, 1\}$ is needed to differentiate whether a state is accepting or not.

(3) Deterministic automata, DA, are coalgebras for $F = 2 \times (\cdot)^A$. The final coalgebra is carried by the set of all languages $2^{A^*}$.

(4) Moore automata, MA, are a slight generalisation of deterministic automata with observations $O$: they are coalgebras for $F = O \times (\cdot)^A$. The final coalgebra is carried by the set of all $O$-valued languages $O^{A^*}$.
(5) Reactive probabilistic labelled transition systems, RPLTS, are coalgebras for $F = (\mathcal{D}(\cdot) + 1)^A$. Behavioural equivalence coincides with Larsen-Skou bisimilarity [LS91].

(6) (Rabin) Probabilistic automata [Rab63], PA, are coalgebras for $F = [0, 1] \times \mathcal{D}(\cdot)^A$.

The following definition generalises the examples above.

**Definition 6.1** (Systems and Automata with M-effects). Let $M$ be a monad and $O$ be a set. We call an $M^A$-coalgebra a system with M-effects, and we call an $O \times M^A$-coalgebra an automaton with M-effects and observations in $O$. We write $c = \langle o, t \rangle$ for an automaton with M-effects and observations in $O$, where $o: X \to O$ is the observation map assigning observations to states, and $t: X \to (MX)^A$ is the transition structure.

For instance, LTS are systems with $\mathcal{P}$-effects while NA are automata with $\mathcal{P}$-effects and observations in 2. Similarly, RPLTS are systems with $\mathcal{D} + 1$-effects, while PA are automata with $\mathcal{D}$-effects and observations in $[0, 1]$. Both DA and MA are automata with no effects ($M = \text{Id}$) and observations in 2 and $O$, respectively.

We write $x \xrightarrow{a} m$ for $t(x)(a) = m$ with $a \in A, x \in X, m \in MX$ in a system or automaton with M-effects. We also write $x \downarrow o_x$ for $o(x) = o_x$ with $o_x \in O$. For an LTS $t: X \to (\mathcal{P}X)^A$ we also write, as usual, $x \xrightarrow{a} y$ for $y \in t(x)(a)$ and $x \not\xrightarrow{a}$ if $t(x)(a) = \emptyset$; for an RPLTS $t: X \to (\mathcal{D}X + 1)^A$, we may also write $x \xrightarrow{a}_p y$ for $t(x)(a)(y) = p$ and again $x \not\xrightarrow{a}$ if $t(x)(a) = \star$. Note that in all our examples of systems and automata there is an implicit finite branching property ensured by the use of $\mathcal{P}$ and $\mathcal{D}$ involving only finite subsets and finitely supported distributions.

**6.2. Determinising Automata with M-effects and Observations in O.** The construction of generalised determinisation was originally discovered in [SBBR10, Bar04]. It enables us to obtain trace semantics for coalgebras of type $c: X \to FMX$ where $F$ is a functor and $M$ a monad. The result is a determinised $F$-coalgebra $c^\#: MX \to FMX$ and the semantics is derived from behavioural equivalence for $F$-coalgebras.

Let $c: X \to FMX$ be a coalgebra and $\lambda: MF \Rightarrow FM$ a functor distributive law. Then the determinisation is the $F$-coalgebra

$$c^\# = MX \xrightarrow{Mc} MFMX \xrightarrow{\lambda} FMMX \xrightarrow{F\mu} FMX. \quad (6.1)$$

It is easy to show that $c^\# \circ \eta = c$ which justifies the notation $c^\#$: the carrier $MX$ carries the $M$-algebra $\mu_X: MMX \to MX$, the free $M$-algebra generated by $X$, $FMX$ carries the $M$-algebra $F\mu \circ \lambda: MFMX \to FMX$, and $c^\#$ is the unique extension of $c$ to a homomorphism from the free $M$-algebra $(MX, \mu)$ to the $M$-algebra $(FMX, F\mu \circ \lambda)$.

In this paper, we only consider determinisation of automata with M-effects and observations in $O$, namely, $FM$-coalgebras for the Moore-automata functor $F = O \times (\cdot)^A$, where $O$ is some set of observations. The following proposition shows that determinising automata with M-effects and observations in $O$ is always possible when the observations carry an $M$-algebra [SBBR10, JSS15].

**Proposition 6.2.** For an Eilenberg-Moore algebra $a: MO \to O$, for $F = O \times (\cdot)^A$ and any monad $M$ on Sets there is a canonical distributive law $\lambda: MF \Rightarrow FM$ given by

$$M(O \times X^A) \xrightarrow{\langle M\pi_1, M\pi_2 \rangle} MO \times M(X^A) \xrightarrow{a \times st} O \times (MX)^A$$
(2) *Behavioural equivalence for (X, c) implies language equivalence.*

(3) *Up-to context is a compatible [PS12] proof technique.*

The second item will be exploited in Section 7 to show that convex bisimilarity implies trace equivalence for NPLTS, while the third item will be fundamental in Section 7.2 to prove the soundness of an effective proof technique. Below we give a more concrete description of the overall construction by relying on a presentation $(\Sigma, E)$ for the monad $M$.

For an $n$-ary operation symbol $f \in \Sigma$ and a $(\Sigma, E)$-algebra $\mathbb{A} = (A, \Sigma_A)$ we write $f^A$ for the $n$-ary operation on $A$ that is the interpretation of $f$. We have that $c^\sharp = \langle o^\sharp, t^\sharp \rangle$ can be defined as follows.

$$ \begin{aligned} o^{\sharp}(x) &= o(x) & o^{\sharp}(f^{MX}(s_1, \dots, s_n)) &= f^{O}(o^{\sharp}(s_1), \dots, o^{\sharp}(s_n)) \\ t^{\sharp}(x) &= t(x) & t^{\sharp}(f^{MX}(s_1, \dots, s_n))(a) &= f^{MX}(t^{\sharp}(s_1)(a), \dots, t^{\sharp}(s_n)(a)) \end{aligned} \qquad (6.3) $$

**Remark 6.5.** Technically, the above definition is telling us that $o^\sharp: MX \to O$ is the unique $M$-algebra homomorphism extending the function $o: X \to O$ and similarly for $t^\sharp: MX \to MX^A$. Such a definition (of a function on $E$-equivalence classes of $\Sigma$-terms) can also be seen as arising from an inductively defined function on $\Sigma$-terms. To be precise, it is important to recall that defining a function over equivalence classes based on representatives always requires to check whether the function is well-defined, in the sense that it is independent of the choice of a representative. Fortunately enough, monad properties guarantee that $o^\sharp: MX \to O$ and $t^\sharp: MX \to MX^A$ are well-defined in this respect<fnref n="5" /> and thus (6.3) can effectively be thought of as an inductive definition on terms. In the remainder of this paper, we will instantiate (6.3) to several examples in this way, without mentioning again that $o^\sharp$ and $t^\sharp$ are well-defined.

The $M$-algebra structure over the final $F$-coalgebra is given for $\varphi_i \in O^{A^*}$ and $w \in A^*$ as

$$ f^{O^{A^*}}(\varphi_1, \dots, \varphi_n)(w) = f^O(\varphi_1(w), \dots, \varphi_n(w)) $$

The fact that $[\cdot]_{c^\sharp}: MX \to O^{A^*}$ is an $M$-algebra homomorphism just means that

$$ [f^{MX}(s_1, \dots, s_n)]_{c^\sharp} = f^{O^{A^*}}([s_1]_{c^\sharp}, \dots, [s_n]_{c^\sharp}) \qquad (6.4) $$

for all $n$-ary operator $f$ in $\Sigma$. Clearly this fact immediately entails that $\approx$ is a congruence w.r.t. the operations in $\Sigma$.

**Example 6.6 (Determinisation of Nondeterministic Automata).** Applying this construction to $F = 2 \times (\cdot)^A$ and $M = \mathcal{P}$, one transforms $c: X \to 2 \times (\mathcal{P}X)^A$ into $c^\sharp: \mathcal{P}X \to 2 \times (\mathcal{P}X)^A$. The former is a nondeterministic automaton and the latter is a deterministic automaton which has $\mathcal{P}X$ as states space. The set of all languages $2^{A^*}$ (seen as functions in $2 = \{0,1\}$) carries the final $F$-coalgebra $\langle \epsilon, \text{der} \rangle: 2^{A^*} \to 2 \times (2^{A^*})^A$ which is exactly the emptiness operation and the derivatives operations by Brzozowski [Brz64]. The final coalgebra morphism $[\cdot]_{c^\sharp}: \mathcal{P}X \to 2^{A^*}$ maps each state of the determinised automaton into the language that it accepts.

In [SBBR10], see also [JSS15], it is shown that, using the distributive law from Proposition 6.2, as $2 = \mathcal{P}1$ is the carrier of the free $\mathcal{P}$-algebra $\mu_1: \mathcal{P}1 \to \mathcal{P}1$, this amounts exactly to the standard determinisation from automata theory and justifies the term *generalised determinisation*.

<footnote n="5">⁵It is enough to observe that (a) the function $\hat{o}^\sharp: T_\Sigma X \to O$ defined inductively on terms in $T_\Sigma X$ is the unique $\Sigma$-algebra homomorphism extending $o$; (b) that there is a monad quotient $q^E: T_\Sigma \Rightarrow M$ and (c) $q_X^E: T_\Sigma X \to MX$ is a $\Sigma$-algebra homomorphism. By uniqueness, $\hat{o}^\sharp = o^\sharp \circ q_X^E$.</footnote>
Recalling that $\mathcal{P}$ is presented by the algebraic theory of semilattices with bottom gives us a more concrete understanding. The set of observations $2 = \{0, 1\}$ carries the semilattice with bottom $0 \sqsubseteq 1$ with supremum operation denoted by $\sqcup$. The interpretation of $\oplus$ and $\star$ in this algebra are defined for all $b_1, b_2 \in 2$ as

$$b_1 \oplus^2 b_2 = b_1 \sqcup b_2 \qquad \star^2 = 0.$$

By instantiating (6.3), one has that the determinisation $c^{\#} = \langle o^{\#}, t^{\#} \rangle: \mathcal{P}X \to 2 \times (\mathcal{P}X)^A$ is defined inductively for all $S \in \mathcal{P}X$ and $a \in A$ as

$$\begin{aligned} o^{\#}(S) &= \left\{ \begin{array}{ll} o(x) & \text{if } S = \eta(x); \\ \star^2 & \text{if } S = \star^{\mathcal{P}X}; \\ o^{\#}(S_1) \oplus^2 o^{\#}(S_2) & \text{if } S = S_1 \oplus^{\mathcal{P}X} S_2; \end{array} \right. \\ = & \left\{ \begin{array}{ll} o(x) & \text{if } S = \{x\}; \\ 0 & \text{if } S = \emptyset; \\ o^{\#}(S_1) \sqcup o^{\#}(S_2) & \text{if } S = S_1 \cup S_2; \end{array} \right. \end{aligned}$$

$$\begin{aligned} t^{\#}(S)(a) &= \left\{ \begin{array}{ll} t(x)(a) & \text{if } S = \eta(x); \\ \star^{\mathcal{P}X} & \text{if } S = \star^{\mathcal{P}X}; \\ t^{\#}(S_1) \oplus^{\mathcal{P}X} t^{\#}(S_2) & \text{if } S = S_1 \oplus^{\mathcal{P}X} S_2; \end{array} \right. \\ = & \left\{ \begin{array}{ll} t(x)(a) & \text{if } S = \{x\}; \\ \emptyset & \text{if } S = \emptyset; \\ t^{\#}(S_1) \cup t^{\#}(S_2) & \text{if } S = S_1 \cup S_2; \end{array} \right. \end{aligned}$$

since $\oplus^{\mathcal{P}X}$ is union of subsets and $\star^{\mathcal{P}X}$ is the empty set. We have seen an example of this construction in Section 1.

The semilattice with bottom over the final $F$-coalgebra $2^{A^*}$ is defined as the pointwise extension of the semilattice over 2, that is, for all $\varphi_1, \varphi_2 \in 2^{A^*}$ and $w \in A^*$

$$(\varphi_1 \oplus^{2^{A^*}} \varphi_2)(w) = \varphi_1(w) \sqcup \varphi_2(w) \qquad \star^{2^{A^*}}(w) = 0$$

Observe that $\oplus^{2^{A^*}}$ is just the union of languages and $\star^{2^{A^*}}$ is the empty language. By instantiating (6.4), one has that

$$[[S_1 \oplus^{\mathcal{P}X} S_2]]_{c^{\#}} = [[S_1]]_{c^{\#}} \oplus^{2^{A^*}} [[S_2]]_{c^{\#}} \qquad [[\star^{\mathcal{P}X}]]_{c^{\#}} = \star^{2^{A^*}}$$

meaning that (a) the language accepted by the union of two sets of states is exactly the union of the languages accepted by the two sets and (b) the empty set accepts the empty language. This immediately entails the first item of Theorem 6.4. The second item, intuitively corresponds to the usual fact that bisimilarity implies language equivalence. The third item allows for exploiting bisimulations up-to $\oplus$ and, consequently, for an efficient algorithm to check language equivalence [BP13].

**Example 6.7** (Determinisation of Probabilistic Automata). Applying the construction for $F = [0, 1] \times (\cdot)^A$ and $M = \mathcal{D}$, one transforms $c: X \to [0, 1] \times (\mathcal{D}X)^A$ into $c^{\#}: \mathcal{D}X \to [0, 1] \times (\mathcal{D}X)^A$. The former is a probabilistic automaton and the latter is a Moore automaton with set of observations $O = [0, 1]$. The set of all $[0, 1]$-valued languages $[0, 1]^{A^*}$ carries the final $F$-coalgebra. Since $[0, 1] = \mathcal{D}(2)$, the set $[0, 1]$ carries the $\mathcal{D}$-algebra $\mu_2: \mathcal{DD}(2) \to \mathcal{D}(2)$ which amounts to taking convex combinations in $[0, 1]$. By exploiting this algebra for the
distributive law in Proposition 6.2, one obtains a final coalgebra semantics that coincides with probabilistic language equivalence of [Rab63] (see [SBBR10]).

Next we illustrate more concretely this construction by relying on the presentation of $\mathcal{D}$ as the algebraic theory of convex algebras. For $p \in [0, 1]$, the interpretation of the operation $+_p$ in $[0, 1]$ is as expected: $q_1+_p^{[0,1]} q_2 = p \cdot q_1 + (1-p) \cdot q_2$. By instantiating (6.3), one has that the determinisation $c^\sharp = \langle o^\sharp, t^\sharp \rangle: \mathcal{D}X \to [0, 1] \times (\mathcal{D}X)^A$ is defined inductively for all $\Delta \in \mathcal{D}X$ and $a \in A$ as

$$ \begin{align*} o^\sharp(\Delta) &= \begin{cases} o(x) & \text{if } \Delta = \eta(x) = \delta_x; \\ o^\sharp(\Delta_1) +_p^{[0,1]} o^\sharp(\Delta_2) & \text{if } \Delta = \Delta_1 +_p^{\mathcal{D}X} \Delta_2; \end{cases} \\ t^\sharp(\Delta)(a) &= \begin{cases} t(x)(a) & \text{if } \Delta = \eta(x) = \delta_x; \\ t^\sharp(\Delta_1) +_p^{\mathcal{D}X} t^\sharp(\Delta_2) & \text{if } \Delta = \Delta_1 +_p^{\mathcal{D}X} \Delta_2; \end{cases} \end{align*} $$

We have seen an example of this construction in Section 1. The convex algebra over the final coalgebra $[0, 1]^{A^*}$ is defined as the pointwise extension of the algebra over $[0, 1]$, that is

$$ (\varphi_1 +_p^{[0,1]^{A^*}} \varphi_2)(w) = \varphi_1(w) +_p^{[0,1]} \varphi_2(w) $$

for $\varphi_1, \varphi_2 \in [0, 1]^{A^*}$ and $w \in A^*$. By instantiating (6.4), one has that

$$ [[\Delta_1 +_p^{\mathcal{D}X} \Delta_2]]_{c^\sharp} = [[\Delta_1]]_{c^\sharp} +_p^{[0,1]^{A^*}} [[\Delta_2]]_{c^\sharp}. $$

We will apply similar methods to obtain languages and language equivalence for automata with both nondeterminism and probability in the rest of the paper.

### 6.3. Invariance of the Semantics.
We next state a theorem that guarantees invariance of the language semantics for automata with M-effects and observations in O, under controlled changes of the monad or the algebra of observations.

**Theorem 6.8 (Invariance Theorem).** Let $(M, \eta, \mu)$ be a monad and $a: MO \to O$ an M-algebra. Let $c = \langle o, t \rangle: X \to O \times (MX)^A$ be an automaton with M-effects and observations in O and $[\cdot]: MX \to O^{A^*}$ be the semantic map induced by the generalised determinisation w.r.t. $a$, i.e., $[\cdot] = [\cdot]_{c^\sharp}$

(1) **Transitions:** Let $(\hat{M}, \hat{\eta}, \hat{\mu})$ be a monad and $\sigma: M \Rightarrow \hat{M}$ a monad map. Let $\hat{a}: \hat{MO} \to O$ be an $\hat{M}$-algebra. Consider the coalgebra

$$ \hat{c} = \langle o, \hat{t} \rangle = \langle o, \sigma_X^A \circ t \rangle: X \to O \times (\hat{MX})^A $$

and let $[\cdot]: \hat{MX} \to O^{A^*}$ be the semantic map induced by its generalised determinisation wrt. $\hat{a}$. If $a = \hat{a} \circ \sigma_O$, then $[\cdot] \circ \eta_X = [\cdot] \circ \hat{\eta}_X$.

(2) **Observations:** Let $\hat{a}: M\hat{O} \to \hat{O}$ be an M-algebra and let $h: (O, a) \to (\hat{O}, \hat{a})$ be an M-algebra morphism. Consider the coalgebra

$$ \hat{c} = \langle \hat{o}, \hat{t} \rangle = \langle h \circ o, t \rangle: X \to \hat{O} \times (MX)^A $$

and let $[\cdot]: MX \to \hat{O}^{A^*}$ be induced by the generalised determinisation wrt. $\hat{a}$. Then $[\cdot] = h^{A^*} \circ [\cdot]$. $\square$

*Proof.* We prove the two items separately:
(1) **Transitions:** The proof proceeds in two steps. First, we show that the following diagram commutes

$$ \begin{tikzcd} MFX \arrow[r, "\sigma_{FX}"] \arrow[d, "\lambda_X"] & \hat{M}FX \arrow[d, "\hat{\lambda}_X"] \\ FMX \arrow[r, "F\sigma_X"] & F\hat{M}X \arrow[d, "\hat{\sigma}_X"] \end{tikzcd} \qquad (6.5) $$

where $\sigma$ is the monad map from the hypothesis, and $\lambda$ and $\hat{\lambda}$ are the distributive laws from Proposition 6.2 used for the determinisation of $FM$- and $F\hat{M}$-coalgebras using the algebras $a$ and $\hat{a}$, and the strengths $st$ and $\hat{st}$, respectively.

The following diagram commutes by naturality of $\sigma$:

$$ \begin{tikzcd} M(X^A) \arrow[r, "\sigma_{X^A}"] \arrow[d, "Mev_a"] & \hat{M}(X^A) \arrow[d, "\hat{M}ev_a"] \\ MX \arrow[r, "\sigma_X"] & \hat{MX} \end{tikzcd} $$

Using this, by definition of the strength, see Proposition 6.2, we have

$$ \begin{align*} (\sigma_X^A \circ st(\varphi))(a) &= \sigma_X^A(st(\varphi)(a)) \\ &= \sigma_X^A(Mev_a(\varphi)) \\ &= (\sigma_X^A \circ Mev_a)(\varphi) \\ \stackrel{(*)}{\implies} &= \hat{M}ev_a \circ \sigma_{X^A}(\varphi) \\ &= \hat{M}ev_a(\sigma_{X^A}(\varphi)) \\ &= \hat{st}(\sigma_{X^A}(\varphi))(a) \\ &= (\hat{st} \circ \sigma_{X^A}(\varphi))(a). \end{align*} $$

where the equality marked by (*) holds by the commutativity of the diagram above. Hence, the following diagram commutes.

$$ \begin{tikzcd} M(X^A) \arrow[r, "\sigma_{X^A}"] \arrow[d, "st"] & \hat{M}(X^A) \arrow[d, "\hat{st}"] \\ (MX)^A \arrow[r, "\sigma_X^A"] & (\hat{MX})^A \end{tikzcd} $$

Recall now that by hypothesis $a = \hat{a} \circ \sigma_O$. Therefore, the following commutes.

$$ \begin{tikzcd} MO \times M(X^A) \arrow[r, "\sigma_O \times \sigma_{X^A}"] \arrow[d, "a \times st"] & \hat{MO} \times \hat{M}(X^A) \arrow[d, "\hat{a} \times \hat{st}"] \\ O \times (MX)^A \arrow[r, "id_O \times \sigma_X^A"] & O \times (\hat{MX})^A \arrow[d, "\hat{id}_O \times \hat{\sigma}_X"] \end{tikzcd} $$
<figure><img src="image_17.png" /></figure>

Now, since $\sigma$ is a monad map, $\hat{\eta} = \sigma \circ \eta$. Therefore $\llbracket \cdot \rrbracket \circ \eta_X = \llbracket \hat{\cdot} \rrbracket \circ \sigma_X \circ \eta_X = \llbracket \hat{\cdot} \rrbracket \circ \hat{\eta}_X$.

(2) **Observations:** Consider the following diagram in Sets.

<figure><img src="image_18.png" /></figure>

Both squares on the left trivially commute by definition. To prove that also the square on the right commutes, it is enough to show that $h^{A*}: O^{A*} \to \hat{O}^{A*}$ coincides with the unique coalgebra morphism $\llbracket \cdot \rrbracket_d$ from the coalgebra

$$d = (h \times \mathrm{id}_{(O^{A*})_A}) \circ \zeta : O^{A*} \to \hat{O} \times (O^{A*})^A$$

to the final $\hat{O} \times (\cdot)^A$-coalgebra $\hat{\zeta}$.

From the inductive definition of $\llbracket \cdot \rrbracket_d$, see Eq. 6.2, we get $\llbracket \varphi \rrbracket_d = \lambda w \in A^*. h \circ \epsilon((\varphi)_w)$ where $(\varphi)_w(u) = \varphi(wu)$ which easily leads to $\llbracket \varphi \rrbracket_d = h \circ \varphi = h^{A*}(\varphi)$.

Now observe that $h \circ o^\sharp$ is equal to $(h \circ o)^\sharp$, since $h$ is an algebra morphism.

From this observation and the commuting of the above diagram, it follows that $h^{A*} \circ \llbracket \cdot \rrbracket$ is the unique coalgebra morphism from $\hat{c}^\sharp = \langle (h \circ o)^\sharp, t^\sharp \rangle$ to the final $\hat{O} \times (\cdot)^A$-coalgebra, and hence it equals $\llbracket \hat{\cdot} \rrbracket$. $\square$

Whenever the monad $M$ has a presentation $(\Sigma, E)$, the first part of the theorem above provides a convenient technique that allows one to work with syntactic terms in $T_\Sigma$ and forget about the axioms in $E$. Let $q^E: T_\Sigma \Rightarrow M$ be the monad morphism quotienting $T_\Sigma$ by the axioms in $E$ and let $r_X: MX \to T_\Sigma X$ be a right inverse of $q_X^E$, namely $q_X^E \circ r_X = \mathrm{id}_{MX}$. Now, the automaton with $M$-effects $c = \langle o, t \rangle: X \to O \times (MX)^A$ can be translated into an automaton with $T_\Sigma$-effects by taking

$$c' = \langle o, t' \rangle = \langle o, r_X^A \circ t \rangle: X \to O \times (T_\Sigma X)^A.$$

Similarly the $M$-algebra of observation $a: MO \to O$ gives rise to the $T_\Sigma$-algebra

$$a' = a \circ q_O^E: T_\Sigma O \to O.$$
Now, rather than determinise *c* with respect to *a*, one can determinise *c'* w.r.t. *a'* and, by virtue of Theorem 6.8.1, the semantics does not change.

**Corollary 6.9.** Let $M$ be a monad with presentation $(\Sigma, E)$. Let $c = \langle o, t \rangle: X \to O \times (MX)^A$ and $c' = \langle o, t' \rangle: X \to O \times (T_\Sigma X)^A$ be such that $q_X^E \circ t' = t$. Let $a: MO \to O$ be an M-algebra. Let $[\cdot]$ and $[\cdot]'$ be the semantics maps induced by the determinisation of $c$ w.r.t. $a$ and, respectively, $c'$ w.r.t. $a' = a \circ q_O^E$. Let $\eta$ and $\eta'$ be the units of $M$ and $T_\Sigma$. Then, $[\cdot] \circ \eta_X = [\cdot]' \circ \eta'_X$.

*Proof.* The property follows immediately by Theorem 6.8.1, but the reader has to be careful not to be mislead: Theorem 6.8.1 cannot be applied to $r_X$, since this is not a monad map (actually, it is not even a natural transformation). The monad map $\sigma: M \Rightarrow \hat{M}$ in the statement of the theorem is the quotient $q^E: T_\Sigma \Rightarrow M$ in the corollary, indeed the monads $M$ and $\hat{M}$ in the theorem correspond to the monads $T_\Sigma$ and $M$ in the corollary, respectively. Similarly, the automaton with $M$-effects $c$ in the theorem is $c'$ in the corollary, while $\hat{c}$ is $c$ in the corollary. The algebras $\hat{a}$ and $a$ in the theorem correspond to $a$ and $a'$ in the corollary, respectively. $\square$

Determinising $c'$ rather than $c$, makes our approach similar to processes calculi. Indeed, in $c'^{\sharp} = \langle o'^{\sharp}, t'^{\sharp} \rangle: T_\Sigma X \to O \times T_\Sigma X^A$, states are syntactic terms rather than elements in $MX$, e.g., sets, distributions, ... The output and transition functions $o'^{\sharp}, t'^{\sharp}$ can be defined by means of GSOS rules. For each $n$-ary operator $f$ in $\Sigma$, we have one rule for output and one rule per action $a \in A$ for transitions:

$$ \frac{s_i \downarrow o_i \quad i \in 1 \dots n}{f(s_1, \dots, s_n) \downarrow f^O(o_1, \dots, o_n)} \qquad \frac{s_i \xrightarrow{a} s'_i \quad i \in 1 \dots n}{f(s_1, \dots, s_n) \xrightarrow{a} f(s'_1, \dots, s'_n)} \qquad (6.6) $$

Here $f^O$ is the interpretation of $f$ in the algebra of observation $a: MO \to O$. For each $x \in X$, we have the following axioms:

$$ \frac{-}{x \downarrow o(x)} \qquad \frac{-}{x \xrightarrow{a} t'(x)(a)} \qquad (6.7) $$

**Remark 6.10.** The rules in (6.6) and (6.7) are equivalent – modulo the axioms in $E$ – to the definition of $o^{\sharp}$ and $t^{\sharp}$ provided by (6.3)$^6$. However, the two rules above provide a specification which is closer to (the standard way of giving) the structured operational semantics via so-called GSOS rules where states are syntactic terms and transitions are derived by the structure of terms. A notable difference, beyond the outputs, is that the transitions specified by (6.6) and (6.7) are deterministic: $s \xrightarrow{a} s'$ means that $t'^{\sharp}(s)(a) = s'$ and not that $s' \in t'(s)(a)$ as common in structured operational semantics.

The connection between GSOS rules and bialgebras was first identified in the seminal work by Turi and Plotkin [DP97]: they show that GSOS rules are in one-to-one correspondence with certain natural transformations that, in turn, give rise to distributive laws of type $\lambda: MF \Rightarrow FM$, see Section 3.3, for $F = \mathcal{P}(\cdot)^A$ and $M$ the term monad $T_\Sigma$ for some signature $\Sigma$. The rules in (6.6) instead can be regarded as a natural transformation $\rho: \Sigma F \Rightarrow F \Sigma$, for $\Sigma$ the functor corresponding to a signature and $F = O \times (\cdot)^A$. In [Kli11], it is shown that natural transformations of this kind, that are named there “simple distributive laws”, give rise to a distributive law of type $\lambda: T_\Sigma F \Rightarrow F T_\Sigma$. In our case, the rules in (6.6) give rise exactly to the distributive law from Proposition 6.2 for $M = T_\Sigma$.

<footnote>$^6$The reader can easily check by induction that $o^{\sharp} \circ q_X^E = o'^{\sharp}$ and that $t^{\sharp} \circ q_X^E = (q_X^E)^A \circ t'^{\sharp}$.</footnote>
6.4. **From Systems to Automata and the Role of Termination.** So far, we have seen how language semantics arises by determinisation of automata. However, our initial interest concerns trace semantics. Trace semantics is closely related to language semantics, but it concerns systems that lack the notion of observation. At the same time, dealing with automata, i.e., having observations, is crucial for determinisation. In this section, we discuss the move from systems to automata that enables defining trace semantics with help of language semantics. The intuition can easily be explained in the case of LTS: Create an automaton from an LTS by making every state accepting. Then trace equivalence for the LTS is language equivalence for the created automaton.

More precisely, starting from an LTS $t: X \to (\mathcal{P}X)^A$, we can add observations in $2 = \mathcal{P}1$ in the simplest possible way, making every state an accepting state:

$$o = (X \xrightarrow{!} 1 \xrightarrow{\eta_1} \mathcal{P}1 = 2)$$

and determinise the NA $\langle o, t \rangle: X \to 2 \times (\mathcal{P}X)^A$ w.r.t. the algebra $\mu_1: \mathcal{P}\mathcal{P}1 \to \mathcal{P}1$. The induced language semantics on the state space $X$ is the standard trace semantics for LTS [BBC$^+$16].

This same approach can be applied in the case of any system with $M$-effects $t: X \to (MX)^A$. We can add observations in $O = M1$ by

$$o = (X \xrightarrow{!} 1 \xrightarrow{\eta_1} M1), \qquad (6.8)$$

determinise the automaton $\langle o, t \rangle$ with $M$-effects using the free algebra on $M1$, and consider the induced language semantics. This idea is summarised in the following definition.

**Definition 6.11** (Trace semantics for systems with $M$-effects). Let $(M, \eta, \mu)$ be a monad and $t: X \to MX^A$ be a system with $M$-effects. Two states $x, y \in X$ are trace equivalent, written $x \equiv y$ iff

$$[[\eta(x)]]_{c^\sharp} = [[\eta(y)]]_{c^\sharp}$$

where $c^\sharp$ is the determinisation w.r.t. $\mu_1: MM1 \to M1$ of $c = \langle o, t \rangle: MX \to M1 \times MX^A$ for $o$ defined as in (6.8).

However, not everything is settled yet, as shown by the following example — the way we model systems, i.e., the choice of the monad involved, may make a huge difference in the semantics that we obtain.

**Example 6.12.** Let us apply Definition 6.11 to an RPLTS $t: X \to (\mathcal{D}X + 1)^A$, namely a system with $\mathcal{D} + 1$-effects. Recall the monad $\mathcal{D} + 1$ from Example 3.2. By taking as sets of observations $O = M1$, one would obtain that $O = \mathcal{D}(1) + 1$ which is isomorphic to 2. Therefore, the final coalgebra would be $2^{A^*}$ making impossible to distinguish probabilistic behaviours.

The problem is not in the choice of observations but already in the monad $\mathcal{D} + 1$. Indeed, even by allowing different observations, determinising w.r.t. such monad would lead a too coarse semantics. Consider for instance the RPLTS in the top of Figure 2. The states $x$ and $y$ should not be trace equivalent, since $x$ has probability $\frac{1}{2}$ of performing trace $ab$, and $y$ has probability $\frac{1}{4}$ of performing trace $ab$. Let us look at what happens, however, if we determinise this system with respect to the monad $\mathcal{D} + 1$. The determinised transition function $t^\sharp$ will give us states in $\mathcal{D}X + 1$, i.e., states that are either full distributions or the element $\star \in 1$ and we have

$$t^{\sharp}(x)(a) = x_1 + \frac{1}{2} x_2 \qquad t^{\sharp}(y)(a) = y_1 + \frac{1}{4} y_2$$
<figure><img src="image_19.png" /><figcaption>Figure 2: An RPLTS (top), part of its determinisation (center) and of its trace semantics (bottom)</figcaption></figure>

However,

$$t^{\#}(x_1 + \frac{1}{2} x_2)(b) = t(x_1)(b) + \frac{1}{2} t(x_2)(b) = \star$$

$$t^{\#}(y_1 + \frac{1}{4} y_2)(b) = t(y_1)(b) + \frac{1}{4} t(y_2)(b) = \star$$

Hence, whatever $(\mathcal{D} + 1)$-algebra of observation we take, these states in the determinised system will return the same observation, i.e., $o^{\#}(x)(ab) = o^{\#}(y)(ab)$. As a consequence, $x$ and $y$ will be equivalent.

The example above suggests that the general trace equivalence given in Definition 6.11 when dealing with systems with effects in a monad of shape $M + 1$ might not provide the best results. Indeed, the state space of the determinised system for such a monad would always be of the shape $MX + 1$, intuitively either an $M$-combination of states in $X$ or $\star \in 1$. The solution that we propose here is to work with the monad $M(\cdot + 1)$ rather than $M + 1$. In order to do this it is enough to recall the morphism $\iota: M + 1 \to M(\cdot + 1)$ from (3.1), transform any system $t: X \to (MX + 1)^A$ into

$$\bar{t}: X \xrightarrow{t} (MX + 1)^A \xrightarrow{\iota_X^A} (M(X + 1))^A \qquad (6.9)$$

and then adopt Definition 6.11. With this recipe, we can recover the appropriate definition of trace equivalence for RPLTS.

**Example 6.13** (Trace semantics for RPLTS). We first turn an RPLTS $t: X \to (\mathcal{D}X + 1)^A$ into a system with $\mathcal{D}(\cdot + 1)$-effects by postcomposing with $\iota^A$, as in (6.9). Observe that the
<figure><img src="image_20.png" /><figcaption>Figure 3: An LTS (top), part of its may-must determinisation (center); and the corresponding may-must semantics (bottom)</figcaption></figure>

monad map $ι: \mathcal{D} + 1 \Rightarrow \mathcal{D}(\cdot + 1)$ only changes the type by embedding distributions into subdistributions and regards the unique element of 1 as the empty subdistribution (namely the one mapping everything to 0).

Now, we can apply Definition 6.11. The set of observation is $[0, 1] = \mathcal{D}(1 + 1)$ equipped with the free $\mathcal{D}(\cdot + 1)$-algebra generated by 1. The observation function $o: X \to [0, 1]$ maps every state $x \in X$ into the element $1 \in [0, 1]$. The function $[[\cdot]]_{c^\sharp} \circ \eta: X \to [0, 1]^{A^*}$ obtained via the generalised determinisation of $c = \langle o, \bar{t} \rangle$ assigns to each state $x \in X$ and trace $w \in A^*$ the probability of reaching from $x$ any other state via $w$. We write $\equiv^{RP}$ for the induced trace equivalence. A similar construction has been used in [FZ14, YJZ17].

Figure 2 illustrates the semantics obtained in this way: observe that, differently from the semantics from Example 6.12, now $x \not\equiv^{RP} y$ since $[[\eta(x)]]_{c^\sharp}(ab) = \frac{1}{2}$ and $[[\eta(y)]]_{c^\sharp}(ab) = \frac{1}{4}$.

For LTS, we have already seen that Definition 6.11 leads to the standard notion of trace semantics. However, by recalling that $\mathcal{P} = \mathcal{P}_{ne} + 1$, one could first transform an LTS into a systems with $\mathcal{P}_{ne}(\cdot + 1)$-effects by (6.9) and then use Definition 6.11. The following example illustrates the alternative trace equivalence obtained in this way.

**Example 6.14** (May/Must trace semantics for LTS). Given an LTS $t: X \to (\mathcal{P}X)^A$, we define $\bar{t}: X \to \mathcal{P}_{ne}(X + 1)^A$ as in (6.9) by recalling that $\mathcal{P} = \mathcal{P}_{ne} + 1$. The embedding $ι_X: \mathcal{P}X \to \mathcal{P}_{ne}(X + 1)$ maps the empty set $\emptyset \in \mathcal{P}X$ into the singleton $\{\star\}$, where $\star$ is the unique element of 1, and any nonempty subset to itself.

To obtain the algebra of observations we take the free $\mathcal{P}_{ne}(\cdot + 1)$-algebra generated by the singleton set $1 = \{\bullet\}$. This is the semilattice

$$ \begin{array}{c} \{\bullet, \star\} \\ \diagdown \\ \{\bullet\} \end{array} \quad (6.10) $$
with point {$\star$}. Hereafter we refer to this as 3. The observation function $o: X \to 3$ maps every state $x \in X$ into the element {$\bullet$} $\in 3$. We rely on a testing scenario to give an intuition of the semantic map $[\cdot]_c^\bullet \circ \eta: X \to 3^{A^*}$ obtained via the generalised determinisation of $c = \langle o, \bar{t} \rangle$: words $w \in A^*$ can be thought as tests to be performed on each state $x \in X$ of the original LTS; the outcome of a test is $\star$ if $x$ does not pass the test, namely it gets stuck during the execution of $w$; the outcome is $\bullet$ if $x$ passes the test, namely it has entirely executed $w$; since the system is nondeterministic different runs of the same test on the same state can lead to different outcomes. If the outcome is always $\bullet$, then $[x]_{c^\bullet}^*(w) = \{\bullet\}$; if it is always $\star$, then $[x]_{c^\bullet}^*(w) = \{\star\}$; if instead the outcome is sometimes $\bullet$ and sometimes $\star$, then $[x]_{c^\bullet}^*(w) = \{\bullet, \star\}$. Figure 3 illustrates an LTS and the obtained semantics. Observe that $[\eta(x')]^*(a) = [\eta(x)]^*(a) = \{\bullet\}$ since both $x$ and $x'$ always pass the test $a$, while $[\eta(x')]^*(b) = [\eta(x)]^*(b) = \{\star\}$ since both $x$ and $x'$ always fail the test $b$. The behaviours of $x'$ and $x$ differ on the test ab: $x'$ always passes ab, while $x$ may fail it. Indeed, by reading $a, x$ can go to $z$ and then get stuck when reading $b$.

We denote the induced equivalence by $\equiv_*^{\text{LTS}}$, and we call it may-must trace equivalence for LTS. Such a name is justified below by introducing may trace and must trace semantics, and in Remark 6.15.

Recall the presentation of the monad $\mathcal{P}_{ne}(\cdot + 1)$ from Section 3.4 and its two possible quotients by the axioms (B) and (T). Let us denote the corresponding quotient maps by $q^B$ and $q^T$, respectively. By applying Definition 6.11 to $(q_X^B)^A \circ \bar{t}$ and $(q_X^T)^A \circ \bar{t}$ one obtains two different semantics which we call may trace equivalence, denoted by $\equiv_B^{\text{LTS}}$, and must trace equivalence, denoted by $\equiv_T^{\text{LTS}}$. To better illustrate both of them, we focus on their algebras of observations.

By quotienting the pointed semilattice (6.10) by (B) and (T), one obtains, respectively, the semilattice with bottom and the semilattice with top freely generated by 1, depicted on the left and on the right below.

$$ \begin{array}{c} \{\bullet\} = \{\bullet, \star\} \\ | \\ \{\star\} \\ \hline \{\bullet\} \end{array} \qquad \begin{array}{c} \{\star\} = \{\bullet, \star\} \\ | \\ \{\bullet\} \end{array} $$

In the semilattice on the left, the top element is assigned when a state $x$ may pass a test $w$, while the bottom element when $x$ always fails. In the semilattice on the right, the top element is assigned when $x$ can fail, while the bottom element is assigned when $x$ always passes the test. Figure 4 illustrates an example of the may semantics and the must semantics.

We conclude by observing that, since the quotient of $\mathcal{P}_{ne}(\cdot + 1)$ by (B) is exactly $\mathcal{P}$ and, since $q^B \circ \iota = \text{id}$, then $\equiv_B^{\text{LTS}}$ is the standard trace semantics for LTS.

**Remark 6.15.** The testing scenario described in Example 6.14, using the three free algebras generated by the singleton set $1 = \{\bullet\}$ as possible outcomes of tests, is exactly the one of the standard theory of testing equivalences [DH84], when taking as class of tests the set of finite traces. Hence, in this testing scenario the equivalences $\equiv_*^{\text{LTS}}$, $\equiv_B^{\text{LTS}}$, and $\equiv_T^{\text{LTS}}$ are respectively the equivalences known as may-must (or test) testing equivalence, may testing equivalence, and must testing equivalence.

In Section 7, we will introduce may-must, may and must semantics for systems with probability and nondeterminism, by basically applying the recipe described in this section to the three monads introduced in Section 5. It is worth to announce here that the obtained
<figure><img src="image_21.png" /><figcaption>Figure 4: May trace (left) and must trace (right) semantics for the LTS in Figure 3</figcaption></figure>

semantics will be “backward compatible” —in a sense that will be clarified later— with $\equiv_{*}^{ LTS}$, $\equiv_{B}^{ LTS}$ and $\equiv_{T}^{ LTS}$. To prove this property we will need the following corollary of Theorem 6.8.

**Corollary 6.16.** Let $(M, \eta, \mu)$ be a submonad of $(\hat{M}, \hat{\eta}, \hat{\mu})$ via an injective monad map $\sigma: M \Rightarrow \hat{M}$. Let $t: X \to (MX)^A$ be a system with M-effects and let $\hat{t}$ be the system with $\hat{M}$-effects $\sigma_X^A \circ t: X \to (\hat{M}X)^A$. Let $\equiv, \equiv\subseteq X \times X$ be the trace equivalences for $t$ and $\hat{t}$, respectively. Then $\equiv = \equiv\square$. $\square$

*Proof.* We fix $o = (X \xrightarrow{!} 1 \xrightarrow{\eta_1} M1)$ and $\hat{o} = (X \xrightarrow{!} 1 \xrightarrow{\hat{\eta}_1} \hat{M1})$.

We first transform the automaton $c = \langle o, t \rangle$ to $\hat{c} = \langle \hat{o}, t \rangle$ and apply Theorem 6.8.2 and then transform $\hat{c} = \langle \hat{o}, t \rangle$ to $\hat{c} = \langle \hat{o}, \hat{t} \rangle$ and apply Theorem 6.8.1.

For the determinisation, take for $a$ in Theorem 6.8.2 the free algebra $\mu_1: MM1 \to M1$ and as $\hat{a}$ the M-algebra $(\hat{\mu} \circ \sigma_{\hat{M1}}): M\hat{M1} \to \hat{M1}$. It is easy to see that $\hat{a}$ is indeed an M-algebra using that $\sigma$ is a monad map, its naturality, and the associativity of $\hat{\mu}$. Since $\sigma$ is a monad map, the following diagram commutes showing that $\sigma_1$ is an M-algebra homomorphism.

<figure><img src="image_22.png" /></figure>

Observe that $\hat{o} = \sigma_1 \circ o$, again since $\sigma$ is a monad map. Then, by Theorem 6.8.2 $\llbracket \hat{\cdot} \rrbracket = \sigma_1^{A*} \circ \llbracket \cdot \rrbracket$ where $\llbracket \cdot \rrbracket$ is the semantics obtained by determinisation of $\hat{c}$ and $\llbracket \cdot \rrbracket$ the one after determinisation of $c$. Since $\sigma_1$ is injective, also $\sigma_1^{A*}$ is injective and we have that for all $x, y \in X$, $\llbracket \eta(x) \rrbracket = \llbracket \eta(\hat{y}) \rrbracket$ iff $\llbracket \eta(x) \rrbracket = \llbracket \eta(\hat{y}) \rrbracket$, i.e., the semantics remains the same.
For the second step, take $\hat{a} = \hat{\mu}: \hat{M}\hat{M}1 \to \hat{M}1$ for the determinisation of $\hat{c}$. By definition $\hat{a} = \hat{a} \circ \sigma_{\hat{O}}$. Therefore Theorem 6.8.1 guarantees that the language semantics of $\hat{c}$ (i.e., trace semantics of $\hat{t}$) again remains the same as the language semantics of $\hat{c}$ (i.e., trace semantics of $t$). $\square$

## 7. MAY / MUST TRACES FOR NPLTS

In this section, we put all the pieces together and give, using the general recipe from Section 6.4, trace semantics for systems featuring nondeterminism, probability, and termination. We work with the monad $T_{\mathcal{P}\mathcal{C}\mathcal{S}} = C(\cdot + 1)$ and consider its two quotients $T_{\mathcal{C}\mathcal{S}\mathcal{B}}$ and $T_{\mathcal{C}\mathcal{S}\mathcal{T}}$ that we have illustrated in Section 5. Each of these choices gives us a meaningful trace equivalence.

We start by recalling three types of coalgebras.

**NPLTS** Nondeterministic probabilistic labelled transition systems, NPLTS, also known as simple Segala systems, are coalgebras for the functor $F = (\mathcal{P}\mathcal{D}(\cdot))^A$. Behavioural equivalence coincides with strong probabilistic bisimilarity [BSV04, Sok11].

**Convex NPLTS** Convex NPLTS are coalgebras for $(C + 1)^A$. Behavioural equivalence coincides with convex probabilistic bisimilarity [Mio14].

**NPA** Nondeterministic Probabilistic automata, NPA, with observations in $O$ are (for us in this paper) coalgebras for $F = O \times (C(\cdot + 1))^A$. We explained in Section 6.4 above how to move from (convex) NPLTS to NPA, which involves two steps: (1) Adding observations and (2) Dealing with termination.

In order to define trace semantics for NPLTS via the general recipe from Section 6.4, we first need to transform them into convex NPLTS which are systems with $C + 1$-effects. Then, following Section 6.4, we transform them into systems with $C(\cdot + 1)$-effects and, finally, we add observations, so to obtain automata with $C(\cdot + 1)$-effects, namely NPA.

We exploit the natural transformations $\text{conv}$ from (4.1) and $\iota$ from (3.1). Given an NPLTS $t: X \to (\mathcal{P}\mathcal{D}X)^A$ we fix

$$ \bar{t} = (X \xrightarrow{t} (\mathcal{P}_{ne}\mathcal{D}X + 1)^A \xrightarrow{(\text{conv}_X + 1)^A} (CX + 1)^A \xrightarrow{\iota_X^A} (C(X + 1))^A) \quad (7.1) $$

and add observations as prescribed in (6.8)

$$ \bar{o} = (X \xrightarrow{!} 1 \xrightarrow{\eta_1} C(1 + 1)) \quad (7.2) $$

Now recall from Proposition 5.1 that the pointed convex semilattice freely generated by 1 is $M_{\mathcal{J},[0,0]}$ and thus $C(1 + 1) = \mathcal{J}$: We easily derive that

$$ \bar{o}(x) = \eta_1(\!(x)) = \eta_1(\bullet) = \{\delta_\bullet\} = [1, 1] $$

for all $x \in X$, as $\delta_\bullet = 1$ (see proof of Proposition 5.1).
Let $\langle \bar{o}^\sharp, \bar{t}^\sharp \rangle: C(X+1) \to \mathcal{J} \times C(X+1)^A$ be the determinisation of $\langle o, t \rangle$ w.r.t. such algebra and $\llbracket \cdot \rrbracket: C(X+1) \to \mathcal{J}^{A^*}$ be the final coalgebra map.

$$
\begin{tikzcd}
& & \mathcal{J} \times C(X+1)^A \arrow[r, "\eta"] & \mathcal{J} \times (\mathcal{J}^{A^*})^A \\
\llbracket \bar{o}, \bar{t} \rrbracket & \arrow[r, "\eta"] & \llbracket \bar{o}^\sharp, \bar{t}^\sharp \rrbracket & \arrow[r, "\eta, \text{der}"] \arrow[dl, "\llbracket \cdot, \cdot \rrbracket"] \\
& & \llbracket \cdot, \cdot \rrbracket^A &
\end{tikzcd}
\qquad
\begin{array}{l}
\llbracket S \rrbracket(\varepsilon) = \bar{o}^\sharp(S) \\
\llbracket S \rrbracket(aw) = \llbracket \bar{t}^\sharp(S)(a) \rrbracket(w)
\end{array}
$$

**Definition 7.1.** We say that two states $x, y \in X$ are may-must trace equivalent, written $x \equiv y$, if and only if $\llbracket \eta(x) \rrbracket = \llbracket \eta(y) \rrbracket$.

By instantiating (6.3) and using the presentation of the monad $C(\cdot + 1)$, we can obtain
a convenient inductive definition of $\langle \bar{o}^\sharp, \bar{t}^\sharp \rangle$:

$$
\bar{o}^{\sharp}(S) = \begin{cases} [1, 1] & \text{if } S = x; \\ [0, 0] & \text{if } S = \star; \\ \bar{o}^{\sharp}(S_1) \min-\max \bar{o}^{\sharp}(S_2) & \text{if } S = S_1 \oplus S_2; \\ \bar{o}^{\sharp}(S_1) +_p \bar{o}^{\sharp}(S_2) & \text{if } S = S_1 +_p S_2. \end{cases}
$$

$$
\bar{t}^{\sharp}(S)(a) = \begin{cases} \bar{t}(x)(a) & \text{if } S = x; \\ \star & \text{if } S = \star; \\ \bar{t}^{\sharp}(S_1)(a) \oplus \bar{t}^{\sharp}(S_2)(a) & \text{if } S = S_1 \oplus S_2; \\ \bar{t}^{\sharp}(S_1)(a) +_p \bar{t}^{\sharp}(S_2)(a) & \text{if } S = S_1 +_p S_2. \end{cases}
$$

**May trace equivalence and must trace equivalence** Now one may want to treat termination in a different way and exploit the monads $T_{\mathcal{ESB}}$ and $T_{\mathcal{ESJ}}$ discussed in Section 5. Given the monad morphisms $q^B: T_{\mathcal{PE_S}} \Rightarrow T_{\mathcal{ESB}}$ and $q^T: T_{\mathcal{PE_S}} \Rightarrow T_{\mathcal{ESJ}}$ quotienting $T_{\mathcal{PE_S}}$ by (B) and (T), respectively, one can construct the transition functions

$$
\bar{t}_B = (q_X^B)^A \circ \bar{t}: X \to (T_{\mathcal{ESB}}X)^A \quad \text{and} \quad \bar{t}_T = (q_X^T)^A \circ \bar{t}: X \to (T_{\mathcal{ESJ}}X)^A. \quad (7.3)
$$

For the observations, we always use the general recipe of Section 6.4 and take the observation
functions:

$$
\bar{o}_B = (X \xrightarrow{!} 1 \xrightarrow{\eta_1} T_{\mathcal{ESB}} 1) \quad \text{and} \quad \bar{o}_T = (X \xrightarrow{!} 1 \xrightarrow{\eta_1} T_{\mathcal{ESJ}} 1).
$$

Recall from Proposition 5.2 and Proposition 5.3 that $\mathrm{Max}_B = ([0,1], \max, +_p, 0)$ and $\mathrm{Min}_T = ([0,1], \min, +_p, 0)$ are, the free convex semilattice with bottom and, respectively, with top, generated by the singleton set 1. Therefore these algebraic structures gives us the determinisation of $\bar{o}_B$ and $\bar{o}_T$. Since $\bar{o}_B(x) = 1$ and $\bar{o}_T(x) = 1$ for all $x \in X$, the determinisation $\bar{o}_B^\sharp: T_{\mathcal{ESB}}X \to [0,1]$ and $\bar{o}_T^\sharp: T_{\mathcal{ESJ}}X \to [0,1]$ enjoy the following inductive definition.

$$
\bar{o}_B^\sharp(S) = \begin{cases} 1 & \text{if } S = x; \\ 0 & \text{if } S = \star; \\ \bar{o}^\sharp(S_1) \max \bar{o}^\sharp(S_2) & \text{if } S = S_1 \oplus S_2; \\ \bar{o}^\sharp(S_1) +_p \bar{o}^\sharp(S_2) & \text{if } S = S_1 +_p S_2. \end{cases}
$$
$$ \bar{o}_T^\sharp(S) = \begin{cases} 1 & \text{if } S = x; \\ 0 & \text{if } S = \star; \\ \bar{o}^\sharp(S_1) \min \bar{o}^\sharp(S_2) & \text{if } S = S_1 \oplus S_2; \\ \bar{o}^\sharp(S_1) +_p \bar{o}^\sharp(S_2) & \text{if } S = S_1 +_p S_2. \end{cases} $$

The transition functions $\bar{t}_B^\sharp : T_{CSB} X \to (T_{CSB} X)^A$ and $\bar{t}_T^\sharp : T_{CSJ} X \to (T_{CSJ} X)^A$ are defined in the same way like $\bar{t}^\sharp$ above.

The coalgebras $\langle \bar{o}_B^\sharp, \bar{t}_B^\sharp \rangle$ and $\langle \bar{o}_T^\sharp, \bar{t}_T^\sharp \rangle$ give rise to morphisms $[[\cdot]]_B : T_{CSB} X \to [0, 1]^{A^*}$ and $[[\cdot]]_T : T_{CSJ} X \to [0, 1]^{A^*}$ and corresponding behavioural equivalences.

**Definition 7.2.** The *may trace equivalence* for the NPLTS is denoted by $\equiv_B$ and defined as

$$ x \equiv_B y \Leftrightarrow [[\eta(x)]]_B = [[\eta(y)]]_B $$

where $\eta$ is the unit of the monad $T_{CSB}$. The *must trace equivalence* for the NPLTS is denoted by $\equiv_T$ and defined by

$$ x \equiv_T y \Leftrightarrow [[\eta(x)]]_T = [[\eta(y)]]_T $$

for $\eta$ denoting now the unit of the monad $T_{CSJ}$.

**Remark 7.3.** One might exploit the generalised determinisation in different ways, but these always lead to the above semantics.

Consider the coalgebra $\langle \bar{o}_B, \bar{t} \rangle : X \to T_{CSB} 1 \times (T_{PCS} X)^A$ and observe that the algebra $\mathrm{Max}_B = ([0, 1], \max, +_p, 0)$, namely $\mu_1 : T_{CSB} T_{CSB} 1 \to T_{CSB} 1$, is also a pointed convex semilattice—formally this is $\mu_1 \circ q^B : T_{PCS} T_{CSB} 1 \to T_{CSB} 1$. One could thus perform the generalised determinisation w.r.t. this algebra and the monad $T_{PCS}$ and obtain an equivalence that we denote by $\equiv'_B$. Theorem 6.8.1 guarantees however that $\equiv'_B = \equiv_B$. Similarly, one could start with the coalgebra $\langle \bar{o}_T, \bar{t} \rangle$, apply the same construction and end up with an equivalence which, by Theorem 6.8.1, coincides with $\equiv_T$.

**Remark 7.4.** By recalling that the monad $C(\cdot + 1)$ is presented by the algebraic theory $\mathcal{P}CS = (\Sigma_{NP} \cup \Sigma_T, E_{NP})$, one can use Corollary 6.9 to determinise w.r.t. the term monad $T_{\Sigma_{NP} \cup \Sigma_T}$ without changing the resulting semantics. The states of the systems determinised in this way are now syntactic terms, i.e, without the axioms in $E_{NP}$, and the determinisation can be expressed by means of GSOS rules. Indeed, by instantiating the GSOS rules (6.6) and (6.7) for an arbitrary signature to the signature $\Sigma_{NP} \cup \Sigma_T$, one obtains exactly the rules displayed in Table 1.

The rule on the right in (6.6) gives rise to the rules for $\star$, $\oplus$ and $+_p$ in Table 1.(a). The rule on the left gives rise to the rules for $\star$, $\oplus$ and $+_p$ in Table 1.(b), (c) and (d) when taking as algebras of observations $\mathrm{Max}_B$, $\mathrm{Min}_T$ and $\mathrm{M}_{[0,0]}$, respectively.

The rules in (6.7) require more explanation. In the rule on the left, $o$ should be instatiated with $\bar{o}_B$, $\bar{o}_T$ and $\bar{o}$. By recalling that for all $x \in X$, $\bar{o}_B(x) = \bar{o}_T(x) = 1$ and $\bar{o}(x) = [1, 1]$ one obtains the rules for $x$ in Table 1.(b), (c) and (d). In order to see that the rule on the right of (6.7) gives rise to the rule for $x$ in Table 1.(a), one should take $t'$ as $(\mathrm{term}_X)^A \circ t$ and observe that $(q_X^{\mathrm{ENP}})^A \circ t'$ coincides with $\bar{t}$.
**Example 7.5.** Consider the convex closure of the NPLTS from Figure 1. Following Remark 7.4, we can syntactically describe the convex sets of subdistributions reached by a state when performing a transition as follows:

$$x \xrightarrow{a} x_1 \oplus (x_3 + \frac{1}{2} x_2)$$

$$y \xrightarrow{a} y_1 \oplus (y_4 + \frac{1}{2} y_2) \oplus ((y_2 + \frac{1}{2} y_4) + \frac{1}{2} y_3)$$

$$x_1 \xrightarrow{b} x + \frac{1}{2} x_3$$

$$y_1 \xrightarrow{b} y + \frac{1}{2} y_4$$

$$x_2 \xrightarrow{b} x_3$$

$$x_2 \xrightarrow{c} x$$

$$y_2 \xrightarrow{b} y_4$$

$$y_3 \xrightarrow{c} y$$

In the determinised system, we have

$$x \xrightarrow{a} S_1 \xrightarrow{b} S_2$$

$$y \xrightarrow{a} S'_1 \xrightarrow{b} S'_2$$

For

$$S_1 = x_1 \oplus (x_3 + \frac{1}{2} x_2)$$

$$S_2 = (x + \frac{1}{2} x_3) \oplus (\star + \frac{1}{2} x_3)$$

$$S'_1 = y_1 \oplus (y_4 + \frac{1}{2} y_2) \oplus ((y_2 + \frac{1}{2} y_4) + \frac{1}{2} y_3)$$

$$S'_2 = (y + \frac{1}{2} y_4) \oplus (\star + \frac{1}{2} y_4) \oplus ((y_4 + \frac{1}{2} \star) + \frac{1}{2} \star)$$

Consider now the observations associated to the terms in the may-must semantics. We have $\bar{o}^{\#}(x) = [1, 1] = \bar{o}^{\#}(y)$ and hence

$$\bar{o}^{\#}(S_1) = [1, 1] \min-\max([1, 1] + \frac{1}{2} [1, 1]) = [1, 1].$$

Analogously, $\bar{o}^{\#}(S'_1) = [1, 1]$. Furtheron

$$\bar{o}^{\#}(S_2) = ([1, 1] + \frac{1}{2} [1, 1]) \min-\max([0, 0] + \frac{1}{2} [1, 1]) = [\frac{1}{2}, 1]$$

and in the same way we derive $\bar{o}^{\#}(S'_2) = [\frac{1}{4}, 1]$.

Hence, $x$ and $y$ are not may-must trace equivalent: $[[x]](ab) = \bar{o}^{\#}(S_2) \neq \bar{o}^{\#}(S'_2) = [[y]](ab)$.

However, using $\text{Max}_B$, we get $\bar{o}_B^{\#}(S_2) = \bar{o}_B^{\#}(S'_2)$ as the intervals obtained via the may-must observation over $S_2, S'_2$ have the same upper bound 1, which is the value returned by both $\bar{o}_B^{\#}(S_2)$ and $\bar{o}_B^{\#}(S'_2)$. Hence, $[[x]]_B(ab) = \bar{o}_B^{\#}(S_2) = \bar{o}_B^{\#}(S'_2) = [[y]]_B(ab)$. More generally, it holds that $x$ and $y$ are may trace equivalent. We can elegantly prove this by using up-to techniques, as shown in Section 7.2.

**7.1. Properties of the semantics.** The three notions of trace equivalence for NPLTS that we have introduced above, $\equiv$, $\equiv_B$ and $\equiv_T$, enjoy several desirable properties that, on the one hand, confirm the appropriateness of our semantics and, on the other, provide useful techniques for reasoning about them. In this section we show such properties while in Section 7.2, we illustrate such techniques at work.
### 7.1.1. Bisimilarity implies trace equivalence.
For NPLTS, there exist two main notions of bisimilarity, which are usually called (strong) probabilistic bisimilarity and convex probabilistic bisimilarity [SL94]. Originally, these relations were called (strong) bisimulation and (strong) probabilistic bisimulation, respectively. We show here that both imply may-must, may, and must trace equivalence. For this purpose, we will repeatedly use the following result from the general theory of coalgebra.

**Lemma 7.6.** [Theorem 15.1 [Rut00]] Let $F$ and $G$ be two endofunctors on Sets and $c: X \to FX$ be an $F$-coalgebra. If there exists a natural transformation $\alpha: F \Rightarrow G$, then behavioural equivalence for $c$ implies behavioural equivalence for $\alpha \circ c$. $\square$

**Theorem 7.7.** Probabilistic bisimilarity (called bisimilarity in the original paper) and convex probabilistic bisimilarity (called probabilistic bisimilarity in the original paper) from [SL94] imply $\equiv$, $\equiv_B$, and $\equiv_T$.

*Proof.* Given an NPLTS, namely a coalgebra $t: X \to (\mathcal{P}DX)^A$, we know from [BSV04, Sok11] that probabilistic bisimilarity of [SL94] (denoted $\approx^p$) coincides with behavioural equivalence. Moreover, by [Mio14], behavioural equivalence for $(\text{conv}_X+1)^A \circ t$ coincides with convex probabilistic bisimilarity ($\approx^c$). Using Lemma 7.6 twice, we have that $\approx^p \subseteq \approx^c \subseteq \approx^t$ where $\approx^t$ is behavioural equivalence for $t_X^A \circ (\text{conv}_X+1)^A \circ t$, namely $\bar{t}$ from (7.1).

Now, by postcomposing $\bar{t}$ with the natural transformation $C(\cdot+1)^A \stackrel{\cong}{\Rightarrow} 1 \times C(\cdot+1)^A \stackrel{\eta_1 \times id}{\Rightarrow} C(1+1) \times C(\cdot+1)^A$ instantiated at $X$, one obtains exactly $c = \langle \bar{o}, \bar{t} \rangle$. Again by Lemma 7.6, $\approx^t \subseteq \approx$ where $\approx$ denotes here behavioural equivalence for $c$. By Theorem 6.4.2, we now can conclude that $\approx \subseteq \equiv$. A similar argument applies for $\equiv_B$ and $\equiv_T$. $\square$

### 7.1.2. Backward compatibility.
Both LTS and RPLTS can be regarded as special cases of NPLTS: LTS are NPLTS where all distributions are Dirac distributions; RPLTS are NPLTS where all subsets are at most singletons. Formally, we can express this using the natural transformations $\mathcal{P}_{ne}\eta^\mathcal{D}: \mathcal{P}_{ne} \Rightarrow \mathcal{P}_{ne}\mathcal{D}$ and $\eta^{\mathcal{P}_{ne}\mathcal{D}}: \mathcal{D} \Rightarrow \mathcal{P}_{ne}\mathcal{D}$. Given an LTS $t: X \to (\mathcal{P}X)^A$ we call

$$ \tilde{t} = X \xrightarrow{t} (\mathcal{P}_{ne}X + 1)^A \xrightarrow{(\mathcal{P}_{ne}\eta_X^\mathcal{D}+1)^A} (\mathcal{P}_{ne}\mathcal{D}X + 1)^A $$

the corresponding NPLTS. Similarly, the NPLTS corresponding to an RPLTS $t: X \to (\mathcal{D}X + 1)^A$ is

$$ \tilde{t} = X \xrightarrow{t} (\mathcal{D}X + 1)^A \xrightarrow{(\eta^{\mathcal{P}_{ne}\mathcal{D}}X+1)^A} (\mathcal{P}_{ne}\mathcal{D}X + 1)^A $$

The following two theorems state that $\equiv_B$, $\equiv_T$, and $\equiv$ generalize—through these translations—the trace equivalences for RPLTS and LTS introduced in Example 6.13 and Example 6.14.

**Theorem 7.8 (Backward Compatibility for RPLTSs).** Let $\equiv^{RP}$ be trace equivalence defined on an RPLTS $t$ and $\equiv_B$, $\equiv_T$ and $\equiv$ the may, must and may-must equivalences defined on the corresponding NPLTS $\tilde{t}$. Then

$$ \equiv^{RP} = \equiv = \equiv_B = \equiv_T $$

*Proof.* We prove $\equiv^{RP} = \equiv$ by applying Corollary 6.16 to the injective monad map $\chi^\mathcal{D}(\cdot + 1)$ from Lemma 5.4. In order to do so, it is enough to observe that the following diagram
commutes: the two triangles by definition of $\tilde{t}$ and $\chi^D$ from Lemma 4.1; the square by Lemma 3.4.

<figure><img src="image_23.png" /></figure>

In the diagram above, the topmost arrow is exactly $\tilde{t}: X \to \mathcal{D}(X+1)^A$ used to define $\equiv^{RP}$ over $t$ (Example 6.13). The down-and-right arrow $\iota_X^A \circ (\mathrm{conv}_X+1)^A \circ \tilde{t}$ is exactly the arrow $\tilde{t}$ used to define $\equiv$ over $\tilde{t}$, see (7.1). Commutativity of the above diagram states that $(\chi^D(\cdot+1))^A \circ \tilde{t} = \tilde{t}$ which, by Corollary 6.16 entails that $\equiv^{RP} = \equiv$.

To prove $\equiv^{RP} = \equiv_B$ we use Corollary 6.16 with the injective monad map $q_X^B \circ \chi^D(\cdot+1)_X$ from Example 5.4. Observe that the commutativity of the above diagram gives us also that $(q_X^B \circ \chi^D(\cdot+1)_X)^A \circ \tilde{t} = (q_X^B)^A \circ \tilde{t}$ and that $(q_X^B)^A \circ \tilde{t}$ is exactly the system used to define $\equiv_B$ on $\tilde{t}$, see (7.3).

The proof for $\equiv^{RP} = \equiv_T$ is obtained by replacing in the previous paragraph B by T. $\square$

<figure><img src="image_24.png" /></figure>

**Theorem 7.9** (Backward Compatibility for LTSs). Let $\equiv_B^{LTS}$, $\equiv_T^{LTS}$, and $\equiv_*^{LTS}$ be may, must, and may-must trace equivalences on an LTS t and $\equiv_B$, $\equiv_T$, and $\equiv$ the equivalences defined on the corresponding NPLTS $\tilde{t}$. Then

$$ \equiv_*^{LTS} = \equiv \qquad \equiv_B^{LTS} = \equiv_B \qquad \equiv_T^{LTS} = \equiv_T $$

*Proof.* The proof for $\equiv_*^{LTS} = \equiv$ is like the one for $\equiv^{RP} = \equiv$, but replacing $\mathcal{D}$ by $\mathcal{P}_{ne}$. The proof for $\equiv_B$ requires one additional step: in the diagram below, the rightmost square commutes by Lemma 5.4.3.

<figure><img src="image_25.png" /></figure>

Like in the case of RPLTS, the two triangles commute by definition of $\tilde{t}$ and $\chi^B_{ne}$ and the central square by Lemma 3.4. So, the whole diagram commutes. Observe that the topmost arrow is exactly $(q_X^B)^A \circ \tilde{t}$ used to define $\equiv_B^{LTS}$ over $t$ (Example 6.14). The down-and-right arrow $(q_X^B)^A \circ \iota_X^A \circ (\mathrm{conv}_X+1)^A \circ \tilde{t}$ is exactly the arrow $(q_X^B)^A \circ \tilde{t}$ used to define $\equiv_B$ over $\tilde{t}$ (see (7.3)). By using Corollary 6.16 with the injective monad map $e_B$ from Lemma 5.4, we obtain that $\equiv_B^{LTS} = \equiv_B$. The proof for $\equiv_T^{LTS} = \equiv_T$ is obtained by replacing in the previous paragraph B by T. $\square$

<figure><img src="image_26.png" /></figure>
7.1.3. The bialgebra of probabilistic traces. The generalised determinisation outlined in Section 6.2 allows to think of the final coalgebra as a denotational universe of behaviours and of the final map [[·]] as a denotational semantics assigning to each state its behaviour. We better illustrate this idea here by considering the may-must semantics, but the same arguments hold for the may and the must cases.

The set $\mathcal{J}^{A^*}$ of nondeterministic-probabilistic languages, namely functions $\varphi: A^* \to \mathcal{J}$, carries at the same time the final coalgebra $\langle \epsilon, \text{der} \rangle: \mathcal{J}^{A^*} \to \mathcal{J} \times \mathcal{J}^{A^*}$ (defined as in Section 6.2 for $O = \mathcal{J}$) and a pointed convex semilattice. The latter is defined as the pointwise extension of the algebra of observations $M_{\mathcal{J},[0,0]}$, see Proposition 5.1. This means that the structure of pointed convex semilattice is defined as follows for all $\varphi_1, \varphi_2 \in \mathcal{J}^{A^*}$ and for all $w \in A^*$.

$$ 
\begin{align*}
(\varphi_1 \oplus^{\mathcal{J}^{A^*}} \varphi_2)(w) &= \varphi_1(w) \min-\max \varphi_2(w) \\
(\varphi_1 +_{p}^{\mathcal{J}^{A^*}} \varphi_2)(w) &= \varphi_1(w) +_{p}^{\mathcal{J}} \varphi_2(w) \\
\star^{\mathcal{J}^{A^*}} (w) &= [0, 0]
\end{align*}
$$

By the generalised determinisation, we know that the final coalgebra map $[[\cdot]]: C(X+1) \to \mathcal{J}^{A^*}$ is also a homomorphism of pointed convex semilattices which means that

$$ [[S_1 \oplus S_2]] = [[S_1]] \oplus_{p}^{\mathcal{J}^{A^*}} [[S_2]], [[S_1 +_p S_2]] = [[S_1]] +_{p}^{\mathcal{J}^{A^*}} [[S_2]] \text{ and } [[\star]] = \star^{\mathcal{J}^{A^*}} $$

for all $S_1, S_2 \in C(X+1)$. This guarantees the following result.

**Theorem 7.10.** Let $\cong$, $\cong_B$ and $\cong_T$ be the kernels of $[[\cdot]]$, $[[\cdot]]_B$, and $[[\cdot]]_T$, respectively. Then $\cong$, $\cong_B$, and $\cong_T$ are congruences w.r.t. $\oplus$ and $+_p$.

The theorem above is an instantiation of Theorem 6.4.1 to our construction for NPLTS. By instantiating Theorem 6.4.3, we have the following useful fact.

**Theorem 7.11.** Up-to context is compatible for each of the three equivalences. $\square$

<figure><img src="image_27.png" /></figure>

In the next section, we illustrate the implication of such result. Since $x \equiv y$ iff $\eta(x) \cong \eta(y)$, hereafter we will sometimes write $\equiv$ instead of $\cong$. Similarly for $\equiv_B$ and $\equiv_T$.

7.2. **Coinduction Up-to.** As anticipated in Theorem 7.11, $\equiv$, $\equiv_B$, and $\equiv_T$ can be proved coinductively by means of bisimulation up-to. In order to define uniformly the proof techniques for the three equivalences, we let $\equiv_i$ to range over $\equiv$, $\equiv_B$, and $\equiv_T$; $T_i$ to range over $T_{\mathcal{P}ES}$, $T_{\mathcal{C}SB}$, and $T_{\mathcal{C}ST}$; $\bar{t}_i^\sharp$, over $\bar{t}_i^\sharp$, $\bar{t}_B^\sharp$, and $\bar{t}_T^\sharp$; $\bar{o}_i^\sharp$ over $\bar{o}_i^\sharp$, $\bar{o}_B^\sharp$, and $\bar{o}_T^\sharp$.

**Definition 7.12.** Let $(X, t)$ be an NPLTS and $(T_i X, \langle \bar{o}_i^\sharp, \bar{t}_i^\sharp \rangle)$ the corresponding determinised system. A relation $\mathcal{R} \subseteq T_i X \times T_i X$ is a bisimulation iff for all $(S_1, S_2) \in \mathcal{R}$ it holds that

(1) $\bar{o}_i^\sharp(S_1) = \bar{o}_i^\sharp(S_2)$ and

(2) $\bar{t}_i^\sharp(S_1)(a) \mathcal{R} \bar{t}_i^\sharp(S_2)(a)$ for all $a \in A$.

The coinduction proof principle (see e.g. [BPPR17]) asserts that for all $x, y \in X$, $x \equiv_i y$ iff there exists a bisimulation $\mathcal{R}$ such that $x \mathcal{R} y$.

We can now prove that states $x, y$ in Figure 1 are may trace equivalent by showing that there exists a bisimulation $\mathcal{R}$ such that $x \mathcal{R} y$ on the system determinized using as algebra of observations $\text{Max}_B$.
<figure><img src="image_28.png" /><figcaption>Figure 5: Determinization</figcaption></figure>

**Example 7.13.** Consider the NPLTS $(X, t)$ depicted in Figure 1, and discussed in Example 7.5. Figure 5 shows the determinization of the system, where the terms are, as already partially mentioned in Example 7.5, as follows

$$
\begin{align*}
S_1 &= x_1 \oplus (x_3 + \frac{1}{2} x_2) & S_2 &= (x + \frac{1}{2} x_3) \oplus (\star + \frac{1}{2} x_3) \\
S'_1 &= y_1 \oplus (y_4 + \frac{1}{2} y_2) \oplus ((y_2 + \frac{1}{2} y_4) + \frac{1}{2} y_3) & & \\
S'_2 &= (y + \frac{1}{2} y_4) \oplus (\star + \frac{1}{2} y_4) \oplus ((y_4 + \frac{1}{2} \star) + \frac{1}{2} \star) & & \\
S_3 &= \star \oplus (\star + \frac{1}{2} x) & S'_3 &= \star \oplus (\star + \frac{1}{2} y)
\end{align*}
$$

and the depicted transitions are those given by $\bar{t}^{\sharp}$.

The determinized NPLTS is a system with infinitely many states, which are given by the presence of cycles in the original system. In the determinization of the automaton with algebra of observation $\text{Max}_B$, each state $S$ is assigned an observation $\bar{o}_B^{\sharp}(S) \in [0, 1]$. We prove that $x$ and $y$ are may trace equivalent by exhibiting the following bisimulation $\mathcal{R}$:

$$
\mathcal{R} = \{(x, y), (S_1, S'_1), (S_2, S'_2), (S_3, S'_3)\} \\
\cup \{((S_i + \frac{1}{2n}) \star) \oplus \star, (S'_i + \frac{1}{2n}) \oplus \star\} | 1 \le i \le 3, n \ge 1
$$

The relation satisfies the two clauses required by Definition 7.12 of bisimulation. As it emerges from Figure 5, the clause on transitions (clause 2) is satisfied by each pair in the relation. As to the clause on the observation (clause 1), we can derive as in Example 7.5 that for every pair $(S, S') \in \{(x, y), (S_1, S'_1), (S_2, S'_2), (S_3, S'_3)\}$ it holds $\bar{o}_B^{\sharp}(S) = \bar{o}_B^{\sharp}(S')$.
Finally, clause 1 also holds for the remaining pairs, since for $1 \le i \le 3$ and $n \ge 1$ we have

$$ \bar{o}_B^\sharp((S_i + \frac{1}{2^n} \star) \oplus \star) = (\bar{o}_B^\sharp(S_i) + \frac{1}{2^n} 0) \max 0 = (\bar{o}_B^\sharp(S_i') + \frac{1}{2^n} 0) \max 0 = \bar{o}_B^\sharp((S_i' + \frac{1}{2^n} \star) \oplus \star) $$

Hence, $\mathcal{R}$ is a bisimulation.

As shown in Example 7.5, $x, y$ are not bisimilar if the algebra of observations for the must equivalence, i.e, $\text{Min}_T$, is used instead of the one for the may equivalence, since $\bar{o}_T^\sharp(S_2) \neq \bar{o}_T^\sharp(S_2')$. Analogously, they are not equivalent if we take the may-must algebra of observation $\text{M}_{j,[0,0]}$.

To make this proof principle more effective, one can use *up-to techniques* [Mil89, PS12]. Particularly relevant for us is up-to *contextual closure* which, for all relations $\mathcal{R} \subseteq T_i(X) \times T_i(X)$, is defined inductively by the following rules.

$$ \begin{array}{ccc} \frac{S \mathcal{R} S'}{S Ctx(\mathcal{R}) S'} & - & \frac{* Ctx(\mathcal{R}) *}{* Ctx(\mathcal{R}) *} \\ \frac{S_1 Ctx(\mathcal{R}) S_1'}{S_1 \oplus S_2 Ctx(\mathcal{R}) S_1' \oplus S_2'} & & \frac{S_2 Ctx(\mathcal{R}) S_2'}{S_1 +_p S_2 Ctx(\mathcal{R}) S_1' +_p S_2'} \\ \frac{S_1 Ctx(\mathcal{R}) S_1'}{S_1 +_p S_2 Ctx(\mathcal{R}) S_1' +_p S_2'} & & \frac{S_2 Ctx(\mathcal{R}) S_2'}{S_1 +_p S_2 Ctx(\mathcal{R}) S_1' +_p S_2'} \end{array} $$

**Definition 7.14.** Bisimulations up-to context are defined as in Definition 7.12, but with $Ctx(\mathcal{R})$ instead of $\mathcal{R}$ in point (2).

By virtue of the general theory in [BPPR17], one has that $Ctx$ is a *sound* up-to technique, that is $x \equiv_i y$ iff there exists a bisimulation up-to context $\mathcal{R}$ such that $x \mathcal{R} y$. Actually, the theory in [BPPR17] guarantees a stronger property known as compatibility [San98, Pou07, PS12]. Intuitively, this means that the technique is sound and it can be safely combined with other compatible up-to techniques. We refer the interested reader to [PS12] for a detailed introduction to compatible up-to techniques.

We conclude with an example illustrating a finite bisimulation up-to context witnessing that the states $x$ and $y$ from Figure 1 are in $\equiv_B$.

**Example 7.15.** Consider the NPLTS depicted in Figure 1. We have seen in Example 7.13 how to prove that $x \equiv_B y$ by exhibiting a bisimulation on $(T_{csB}X, \langle\bar{o}_B^\sharp, \bar{t}_B^\sharp\rangle)$ relating them. However, due to the presence of cycles, the determinization of the NPLTS is infinite and the bisimulation relation contains infinitely many pairs.

With bisimulations up-to, only few pairs are necessary. Indeed, we prove that the relation

$$ \mathcal{R} = \{ (x, y), (x_1, y_1), (x_3, y_4), (x_3 + \frac{1}{2} x_2, (y_4 + \frac{1}{2} y_2) \oplus ((y_2 + \frac{1}{2} y_4) + \frac{1}{2} y_3)) \} $$

is a bisimulation up-to context. First, note that the observation is trivially the same for all pairs in the relation, since $\bar{o}_B^\sharp(S) = 1$ for all $S$ in the relation. Heck that the clauses of bisimulation up-to context on the transitions are satisfied. Consider the first pair. In
$(T_{csB}X, \langle \bar{o}_B^\sharp, \bar{t}_B^\sharp \rangle)$, we have

$$x \xrightarrow{a} x_1 \oplus (x_3 + \frac{1}{2} x_2)$$

$$y \xrightarrow{a} y_1 \oplus (y_4 + \frac{1}{2} y_2) \oplus ((y_2 + \frac{1}{2} y_4) + \frac{1}{2} y_3)$$

The reached states are in $Ctx(\mathcal{R})$ by the second and fourth pairs of $\mathcal{R}$. For any action $a' \neq a$, we have $x \xrightarrow{a'} \star, y \xrightarrow{a'} \star$ and $\star Ctx(\mathcal{R}) \star$.

The second and the third pairs can be checked in a similar way. For the fourth pair, we have

$$x_3 + \frac{1}{2} x_2 \xrightarrow{b} \star + \frac{1}{2} x_3$$

$$(y_4 + \frac{1}{2} y_2) \oplus ((y_2 + \frac{1}{2} y_4) + \frac{1}{2} y_3) \xrightarrow{b} (\star + \frac{1}{2} y_4) \oplus ((\star + \frac{1}{2} y_4) + \frac{1}{2} \star)$$

We observe that

$$(\star + \frac{1}{2} y_4) \oplus ((\star + \frac{1}{2} y_4) + \frac{1}{2} \star)$$

$$\stackrel{(B)}{=} (\star + \frac{1}{2} y_4) \oplus ((\star + \frac{1}{2} y_4) + \frac{1}{2} \star) \oplus \star$$

$$\stackrel{(C)}{=} (\star + \frac{1}{2} y_4) \oplus \star$$

$$\stackrel{(B)}{=} \star + \frac{1}{2} y_4$$

and we conclude by $\star + \frac{1}{2} x_3 Ctx(\mathcal{R}) \star + \frac{1}{2} y_4$. The cases for $a$ and $c$ are simpler.

## 8. FROM THE GLOBAL TO THE LOCAL PERSPECTIVE

Usually trace semantics for NPLTS is defined in terms of schedulers, or resolutions: intuitively, a scheduler resolves the nondeterminism by choosing, at each step of the execution of an NPLTS, one of its possible transitions; the transition systems resulting from these choices are called resolutions.

This perspective on trace semantics is somehow opposed to ours, where the generalised determinisation keeps track of all possible executions at once. In this sense, the determinisation provides a perspective which is global, opposite to those of resolutions that are local. In this section, we show that our semantics can be characterised through such local views, by means of resolutions, defined as follows.

**Definition 8.1.** Let $t: X \to (\mathcal{P}DX)^A$ be an NPLTS. A (randomized) resolution for $t$ is a triple $\mathcal{R} = (Y, \text{corr}, r)$ where $Y$ is a set of states, $\text{corr}: Y \to X$ is the correspondence function, and $r: Y \to (DY + 1)^A$ is an RPLTS such that for all $y \in Y$ and $a \in A$,

$$(1) \ r(y)(a) = \star \text{ iff } t(\text{corr}(y))(a) = \star,$$

$$(2) \ \text{if } r(y)(a) \neq \star \text{ then } \mathcal{D}(\text{corr})(r(y)(a)) \in \text{conv}(t(\text{corr}(y))(a)).$$

Intuitively, this means that a resolution of an NPLTS is built from the original system by discarding internal nondeterminism (the possibility to perform multiple transitions labelled with the same action) and in such a way that the structure of the original system is preserved.
<figure><img src="image_29.png" /><figcaption>Figure 6: The resolutions $\mathcal{R}_1$ (left), $\mathcal{R}_2$ (center), and $\mathcal{R}_3$ (right).</figcaption></figure>

**Example 8.2.** Consider the NPLTS on the left of Figure 1. The RPLTSs $\mathcal{R}_1$ and $\mathcal{R}_2$ in Figure 6 are two resolutions for it, both having the identity as correspondence function. In the resolution $\mathcal{R}_1$, the nondeterministic choice of $x$ is resolved by choosing the leftmost $a$-transition. The resolution $\mathcal{R}_2$ is obtained by taking a convex combination of the two distributions $\delta_{x_1}$ and $\Delta_2$, assigning one half probability to each of them.

The reason why we take arbitrary corr functions, rather than just injective ones, is that the original NPLTS might contain cycles, in which case we want to allow the resolution to take different choices at different times.

**Example 8.3.** In order to understand how a resolution allows to resolve differently nonde-terministic choices at different times, when cycles occur in the original system, consider the NPLTS on the left of Figure 1 and its resolution $\mathcal{R}_3$ in Figure 6. In the latter, the state space is enlarged with state $x_4$, which is mapped to $x$ by the correspondence function. On the remaining states, the correspondence function is the identity over $X$. In this resolution, $x$ first chooses the right-hand transition of the original NPLTS, and at the next cycle iteration, represented by $x_4$, the left-hand transition is chosen. Observe that $\text{prob}_{\mathcal{R}_3}(x)(abab) = 0$.

Given a resolution $\mathcal{R} = (Y, \text{corr}, r)$, we define the function $\text{prob}_{\mathcal{R}}: Y \to [0, 1]^{A^*}$ induc- tively for $y \in Y$ and $w \in A^*$ as

$$ \begin{aligned} \text{prob}_{\mathcal{R}}(y)(\varepsilon) &= 1; \\ \text{prob}_{\mathcal{R}}(y)(aw) &= \begin{cases} 0 & \text{if } r(y)(a) = \star; \\ \sum_{y' \in \text{supp}(\Delta)} \Delta(y') \cdot \text{prob}_{\mathcal{R}}(y')(w) & \text{if } r(y)(a) = \Delta. \end{cases} \end{aligned} $$

Intuitively, for all states $y \in Y$, $\text{prob}_{\mathcal{R}}(y)(w)$ gives the probability of $y$ performing the trace $w$. For instance, in the resolutions in Figure 6, $\text{prob}_{\mathcal{R}_1}(x)(abab) = \frac{1}{2}$ and $\text{prob}_{\mathcal{R}_2}(x)(abab) = \frac{3}{16}$.

Now, given an NPLTS $(X, t)$, define $\llbracket \cdot \rrbracket: X \to [0, 1]^{A^*}$ by, for $x \in X$ and $w \in A^*$,

$$ \llbracket x \rrbracket(w) = \bigcup \{ \text{prob}_{\mathcal{R}}(y)(w) \mid \mathcal{R} = (Y, \text{corr}, r) \text{ is a resolution of } (X, t) \text{ and } \text{corr}(y) = x \}. $$

Similarly, we define

$$ \llbracket x \rrbracket(w) = \bigcap \{ \text{prob}_{\mathcal{R}}(y)(w) \mid \mathcal{R} = (Y, \text{corr}, r) \text{ is a resolution of } (X, t) \text{ and } \text{corr}(y) = x \}. $$
The following theorem states that the global view of trace semantics developed in Section 7 coincides with the trace semantics defined locally via resolutions.

**Theorem 8.4 (Global/local correspondence).** Let $(X, t)$ be an NPLTS. For all $x \in X$ and $w \in A^*$, it holds that

$$[[x]](w) = [[\llcorner x \rrcorner](w), [[\llcorner x \rrcorner]](w)].$$

**Corollary 8.5.** Let $(X, t)$ be an NPLTS. For all $x \in X$ and $w \in A^*$, $[[x]]_B(w) = [[\llcorner x \rrcorner]](w)$ and $[[x]]_T(w) = [[\llcorner x \rrcorner]](w)$.

Theorem 8.4 and Corollary 8.5 provide a characterisation of $\equiv$, $\equiv_B$ and $\equiv_T$ in terms of resolutions. Their proofs are presented in section 8.1. Moreover, we show in Section 8.2 that $\equiv_B$ coincides with the randomized $\sqcup$-trace equivalence investigated in [Cas18] and inspired by [BDL14b, BDL14a].

**8.1. Proof of the global/local correspondence theorems.** Given a resolution $\mathcal{R} = (Y, \text{corr}, r)$, we define the function $\text{reach}_{\mathcal{R}}: Y \to (\mathcal{D}(Y+1))^{A^*}$ inductively as

$$\text{reach}_{\mathcal{R}}(y)(\varepsilon) = \delta_y;$$

$$\text{reach}_{\mathcal{R}}(y)(aw) = \begin{cases} \delta_{\star} & \text{if } r(y)(a) = \star; \\ \sum_{y' \in \text{supp}(\Delta)} \Delta(y') \cdot \text{reach}_{\mathcal{R}}(y')(w) & \text{if } r(y)(a) = \Delta. \end{cases}$$

Intuitively, this assigns to each state $y \in Y$ and word $w \in A^*$ a subdistribution over $Y$, which is the state of the determinised system that $y$ reaches via $w$.

Let $o'^{\#}: \mathcal{D}(Y+1) \to [0, 1]$ be the function assigning to a subdistribution $\Delta$ its total mass, namely $1 - \Delta(\star)$. More formally, this is defined inductively as

$$o'^{\#}(\Delta) = \begin{cases} 0 & \text{if } \Delta = \delta_{\star}; \\ 1 & \text{if } \Delta = \delta_y \text{ for } y \in Y; \\ o'^{\#}(\Delta_1) +_p o'^{\#}(\Delta_2) & \text{if } \Delta = \Delta_1 +_p \Delta_2. \end{cases}$$

**Lemma 8.6.** $o'^{\#} \circ \text{reach}_{\mathcal{R}} = \text{prob}_{\mathcal{R}}$.

*Proof.* We prove that $o'^{\#}(\text{reach}_{\mathcal{R}}(y)(w)) = \text{prob}_{\mathcal{R}}(y)(w)$ for all $y \in Y$ and $w \in A^*$. The proof proceeds by induction on $w$.

Base case: $w = \varepsilon$.

$$\text{prob}_{\mathcal{R}}(y)(\varepsilon) = 1 = o'^{\#}(\delta_y) = o'^{\#}(\text{reach}_{\mathcal{R}}(y)(\varepsilon))$$

Inductive case: $w = aw'$. If $r(y)(a) = \star$, then

$$\text{prob}_{\mathcal{R}}(y)(aw') = 0 = o'^{\#}(\delta_{\star}) = o'^{\#}(\text{reach}_{\mathcal{R}}(y)(aw')).$$

If $r(y)(a) = \Delta$, then

$$\text{prob}_{\mathcal{R}}(y)(aw') = \sum_{y' \in \text{supp}(\Delta)} \Delta(y') \cdot \text{prob}_{\mathcal{R}}(y')(w') \quad (\text{definition})$$

$$= \sum_{y' \in \text{supp}(\Delta)} \Delta(y') \cdot o'^{\#}(\text{reach}_{\mathcal{R}}(y')(w')) \quad (\text{IH})$$

$$= o'^{\#}(\sum_{y' \in \text{supp}(\Delta)} \Delta(y') \cdot (\text{reach}_{\mathcal{R}}(y')(w')))) \quad (o'^{\#} \text{ hom.})$$

$$= o'^{\#}(\text{prob}_{\mathcal{R}}(y)(aw')) \quad (\text{definition}).$$
<figure><img src="image_30.png" /></figure>

Given an NPLTS $(X, t)$, we define the function reach: $X \to (C(X+1))^{A^*}$ inductively as
$$ \text{reach}(x)(\varepsilon) = \{\delta_x\}; $$

$$ \text{reach}(x)(aw) = \left\{ \bigoplus_{\Delta \in \text{conv}(S)} \sum_{x' \in \text{supp}(\Delta)} \Delta(x') \cdot \text{reach}(x')(w) \quad \begin{array}{l} \text{if } t(x)(a) = \star; \\ \text{if } t(x)(a) = S. \end{array} \right. $$

For each NPLTS $(X, t)$, we have a function $\langle\langle\cdot\rangle\rangle: C(X+1) \to C(X+1)^{A^*}$ defined for all $S \in C(X+1)$ and $w \in A^*$ as

$$ \langle\langle S \rangle\rangle(\varepsilon) = S; $$

$$ \langle\langle S \rangle\rangle(aw) = \langle\langle \bar{t}^\sharp(S)(a) \rangle\rangle(w). $$

The following property follows directly from the inductive definitions of $\llbracket\cdot\rrbracket$ and $\langle\langle\cdot\rangle\rangle$.

**Lemma 8.7.** $\llbracket\cdot\rrbracket = \bar{o}^\sharp \circ \langle\langle\cdot\rangle\rangle$

**Lemma 8.8.** $\langle\langle\cdot\rangle\rangle \circ \eta = \text{reach}$

*Proof.* The proof goes by induction on $w \in A^*$.

Base case: if $w = \varepsilon$, then $\text{reach}(x)(\varepsilon) = \{\delta_x\} = \eta(x) = \langle\langle\eta(x)\rangle\rangle(\varepsilon)$.

Inductive case: $w = aw'$. If $t(x)(a) = \star$, then $\langle\langle\eta(x)\rangle\rangle(aw') = \langle\langle\bar{t}^\sharp(\{\delta_x\})(a)\rangle\rangle(w') = \langle\langle\{\delta_\star\}\rangle\rangle(w') = \{\delta_\star\} = \text{reach}(x)(aw')$.

If $t(x)(a) = S$, then $\text{reach}(x)(aw) = \bigoplus_{\Delta \in \text{conv}(S)} \sum_{x' \in \text{supp}(\Delta)} \Delta(x') \cdot \text{reach}(x')(w)$. By induction hypothesis, the latter is equal to $\bigoplus_{\Delta \in \text{conv}(S)} \sum_{x' \in \text{supp}(\Delta)} \Delta(x') \cdot \langle\langle\eta(x')\rangle\rangle(w')$. Since $\bar{t}^\sharp$ is a homomorphism of convex semilattices, then $\langle\langle\cdot\rangle\rangle$ is a homomorphism of convex semilattices. Hence, the latter is equal to $\langle\langle\bigoplus_{\Delta \in \text{conv}(S)} \sum_{x' \in \text{supp}(\Delta)} \Delta(x') \cdot \eta(x')\rangle\rangle(w)$ that is $\langle\langle\text{conv}(S)\rangle\rangle(w') = \langle\langle\bar{t}^\sharp(\{\delta_x\})(a)\rangle\rangle(w') = \langle\langle\eta(x)\rangle\rangle(aw')$. $\square$

**Proposition 8.9.** $\llbracket\cdot\rrbracket \circ \eta = \bar{o}^\sharp \circ \text{reach}$

*Proof.* By Lemma 8.7, $\llbracket\cdot\rrbracket \circ \eta = \bar{o}^\sharp \circ \langle\langle\cdot\rangle\rangle \circ \eta$. By Lemma 8.8, $\bar{o}^\sharp \circ \langle\langle\cdot\rangle\rangle \circ \eta = \bar{o}^\sharp \circ \text{reach}$. $\square$

**Proposition 8.10.** Let $(X, t)$ be an NPLTS and let $\mathcal{R} = (Y, \text{corr}, r)$ be one of its resolutions. Let $x \in X$ and $y \in Y$ such that $\text{corr}(y) = x$. For all $w \in A^*$,

$$ \mathcal{D}(\text{corr}+1)(\text{reach}_{\mathcal{R}}(y)(w)) \in \text{reach}(x)(w). $$

*Proof.* By induction on the structure of $w$. If $w = \epsilon$ then

$$ \begin{align*} \mathcal{D}(\text{corr}+1)(\text{reach}_{\mathcal{R}}(y)(\epsilon)) &= \mathcal{D}(\text{corr}+1)(\delta_y) \\ &= \delta_x \\ &\in \{\delta_x\} \\ &= \text{reach}(x)(\epsilon) \end{align*} $$

If $w = aw'$ and $t(x)(a) = \star$, then $r(y)(a) = \star$, and

$$ \begin{align*} \mathcal{D}(\text{corr}+1)(\text{reach}_{\mathcal{R}}(y)(aw')) &= \mathcal{D}(\text{corr}+1)(\delta_\star) \\ &= \delta_\star \\ &\in \{\delta_\star\} \\ &= \text{reach}(x)(aw') \end{align*} $$
If $t(x)(a) \neq \star$ then we have $r(y)(a) \neq \star$. Let $r(y)(a) = \Delta \in \mathcal{D}(Y)$. We have:

$$ 
\begin{aligned}
& \mathcal{D}(\mathrm{corr}+1)(\mathrm{reach}_{\mathcal{R}}(y)(aw')) \\
& = \mathcal{D}(\mathrm{corr}+1)(\sum_{y' \in \mathrm{supp}(\Delta)} \Delta(y') \cdot \mathrm{reach}_{\mathcal{R}}(y')(w')) \\
& = \sum_{y' \in \mathrm{supp}(\Delta)} \Delta(y') \cdot \mathcal{D}(\mathrm{corr}+1)(\mathrm{reach}_{\mathcal{R}}(y')(w'))
\end{aligned}
$$

By the inductive hypothesis, for each $y'$ we have

$$ \mathcal{D}(\mathrm{corr}+1)(\mathrm{reach}_{\mathcal{R}}(y')(w')) \in \mathrm{reach}(\mathrm{corr}(y'))(w'). $$

Hence, by the definition of Minkowski sum,

$$ \sum_{y' \in \mathrm{supp}(\Delta)} \Delta(y') \cdot \mathcal{D}(\mathrm{corr}+1)(\mathrm{reach}_{\mathcal{R}}(y')(w')) \in \sum_{y' \in \mathrm{supp}(\Delta)} \Delta(y') \cdot \mathrm{reach}(\mathrm{corr}(y'))(w') $$

Since $\mathcal{R}$ is a resolution, there is a $\Delta' \in \mathrm{conv}(t(x)(a))$ such that $\mathcal{D}(\mathrm{corr})(\Delta) = \Delta'$. The latter means that $\Delta'(x') = \sum_{\{y' \in \mathrm{supp}(\Delta)|\mathrm{corr}(y')=x'\}} \Delta(y')$, and thus:

$$ \sum_{y' \in \mathrm{supp}(\Delta)} \Delta(y') \cdot \mathrm{reach}(\mathrm{corr}(y'))(w') = \sum_{x' \in \mathrm{supp}(\Delta')} \Delta'(x') \cdot \mathrm{reach}(x')(w') $$

as easily follows from the axioms of convex algebras. We can then conclude by the definition of $\mathrm{reach}(x)(aw')$

$$ 
\begin{aligned}
\sum_{x' \in \mathrm{supp}(\Delta')} \Delta'(x') \cdot \mathrm{reach}(x')(w') &\subseteq \bigoplus_{\Delta' \in \mathrm{conv}(t(a)(x))} \sum_{x' \in \mathrm{supp}(\Delta')} \Delta'(x') \cdot \mathrm{reach}(x')(w') \\
&= \mathrm{reach}(x)(aw').
\end{aligned}
$$

□

**Proposition 8.11.** Let $(X, t)$ be an NPLTS. For all $x \in X$ and $w \in A^*$, if $\Delta \in \mathrm{reach}(x)(w)$ then there exists a resolution $\mathcal{R} = (Y, \mathrm{corr}, r)$ and a state $y \in Y$ such that

(1) $\mathrm{corr}(y) = x$ and

(2) $\mathcal{D}(\mathrm{corr}+1)(\mathrm{reach}_{\mathcal{R}}(y)(w)) = \Delta$.

*Proof.* The proof proceeds by induction on $w \in A^*$.

In the base case $w = \varepsilon$. For all $x \in X$ and $a \in A$ such that $t(x)(a) \neq \star$, we can choose one distribution $\Delta_{x,a} \in t(x)(a)$. Then, we take $\mathcal{R} = (X, id_X, r)$ where $r: X \to (\mathcal{D}X + 1)^A$ is defined for all $x \in X$ and $a \in A$ as

$$ r(x)(a) = \begin{cases} \star & \text{if } t(x)(a) = \star; \\ \Delta_{x,a} & \text{otherwise.} \end{cases} $$

By construction $\mathcal{R}$ is a resolution. Then we take $x$ as the selected state $y$ of the resolution $\mathcal{R}$. Since the correspondence function is $id_X$, (1) is immediately satisfied. Now, by definition, $\mathrm{reach}_{\mathcal{R}}(x)(\varepsilon) = \delta_x$ and $\mathrm{reach}(x)(\varepsilon) = \{\delta_x\}$. We conclude by observing that $\mathcal{D}(id_X + 1)(\delta_x) = \delta_x \in \{\delta_x\} = \mathrm{reach}(x)(\varepsilon)$.

In the inductive case $w = aw'$. Now we have two cases to consider: either $t(x)(a) = \star$ or $t(x)(a) = S$ for $S \in \mathcal{P}_{ne}\mathcal{D}(X)$.
Assume $t(x)(a) = \star$. Then $\text{reach}(x)(aw') = \{\delta_\star\}$. Let $\mathcal{R} = (X, id_X, r)$ be the resolution defined as in the base case, and take $x$ as the selected state $y$ of the resolution $\mathcal{R}$. Since the correspondence function is $id_X$, (1) is immediately satisfied. Since $\mathcal{R}$ is a resolution, $t(x)(a) = \star$ implies $r(x)(a) = \star$. Hence, $\text{reach}_{\mathcal{R}}(x)(a) = \delta_\star$ and $\text{reach}(x)(a) = \{\delta_\star\}$. We conclude by $\mathcal{D}(id_X + 1)(\delta_\star) = \delta_\star \in \{\delta_\star\} = \text{reach}(x)(a)$.

Assume $t(x)(a) = S$. Then

$$ \text{reach}(x)(aw') = \bigoplus_{\Delta' \in \text{conv}(S)} \sum_{x' \in \text{supp}(\Delta')} \Delta'(x') \cdot \text{reach}(x')(w'). $$

By Lemma 4.14, it holds that

$$ \text{reach}(x)(aw') = \bigcup_{\Delta' \in \text{conv}(S)} \sum_{x' \in \text{supp}(\Delta')} \Delta'(x') \cdot \text{reach}(x')(w'). $$

Hence, $\Delta \in \text{reach}(x)(aw')$ if and only if there exists a $\Delta' \in \text{conv}(S)$ such that

$$ \Delta \in \sum_{x' \in \text{supp}(\Delta')} \Delta'(x') \cdot \text{reach}(x')(w'). $$

This is in turn equivalent to saying (by the definition of Minkowski sum) that for every $x' \in \text{supp}(\Delta')$ there exists a $\Delta'_{x'} \in \text{reach}(x')(w')$ such that

$$ \Delta = \sum_{x' \in \text{supp}(\Delta')} \Delta'(x') \cdot \Delta'_{x'}. $$

We can now use the induction hypothesis on $\Delta'_{x'} \in \text{reach}(x')(w')$: for each $\Delta'_{x'} \in \text{reach}(x')(w')$ there exists a resolution $\mathcal{R}_{x'} = (Y_{x'}, \text{corr}_{x'}, r_{x'})$ and a $y_{x'} \in Y_{x'}$ such that

(c) $\text{corr}_{x'}(y_{x'}) = x'$ and

(d) $\mathcal{D}(\text{corr}_{x'} + 1)(\text{reach}_{\mathcal{R}_{x'}}(y_{x'})(w)) = \Delta'_{x'}$.

Now we construct the coproduct of all the resolutions $\mathcal{R}_{x'}$. Take $Z$ to be the disjoint union of all the $Y_{x'}$ and define $\text{corr}_Z: Z \to X$ as $\text{corr}_Z(z) = \text{corr}_{x'}(z)$ if $z \in Y_{x'}$. Similarly, we define $r_Z: Z \to (\mathcal{D}Z + 1)^A$ as $r_Z(z) = r_{x'}(z)$ if $z \in Y_{x'}$. By construction, $\mathcal{R}_Z = (Z, \text{corr}_Z, r_Z)$ is a resolution of $(X, t)$.

Let $\mathcal{R}' = (X, id_X, r')$ be a resolution defined as in the base case, i.e., by arbitrarily choosing a distribution $\Delta_{x,a} \in t(x)(a)$, for any $x$ and $a$, as value of $r'(x)(a)$, whenever $t(x)(a) \neq \star$. We define the resolution $\mathcal{R} = (Y, \text{corr}, r)$ needed to conclude the proof as follows: the state space is $Y = Z + X + \{y\}$, namely the disjoint union of $Z$, of $X$, and of the singleton containing a fresh state $y$; the correspondence function $\text{corr}: Y \to X$ and the transition function $r: Y \to (\mathcal{D}Y + 1)^A$ are defined for all $u \in Y$ as

$$ \text{corr}(u) = \begin{cases} \text{corr}_Z(u) & \text{if } u \in Z, \\ \text{id}_X(u) & \text{if } u \in X, \\ x & \text{if } u = y, \end{cases} \\ r(u)(b) = \begin{cases} r_Z(u)(b) & \text{if } u \in Z, \\ r'(u)(b) & \text{if } u \in X, \\ \Delta_{x,b} & \text{if } u = y, a \neq b, t(x)(b) \neq \star, \\ \star & \text{if } u = y, a \neq b, t(x)(b) = \star, \\ \Delta'' & \text{if } u = y, a = b \end{cases} $$
where $\Delta''$ is the distribution having as support the set of states $\{y_{x'}|x' \in \text{supp}(\Delta)\} \subseteq Z$, and such that $\Delta''(y_{x'}) = \Delta'(x')$. Note that $\Delta''$ is a distribution, since $\Delta'$ is and since we are taking exactly one $y_{x'}$ for each $x' \in \text{supp}(\Delta')$.

The fact that $\mathcal{R}$ is a resolution follows from $\mathcal{R}_Z$ and $\mathcal{R}'$ being resolutions and $y$ respecting
- by construction- the conditions of resolution: indeed $\text{corr}(y) = x$, and

* if $a \neq b$ and $t(x)(b) \neq \star$, then $r(y)(b) = \Delta_{x,b}$ and $\mathcal{D}(\text{corr})(\Delta_{x,b}) = \mathcal{D}(\text{id}_X)(\Delta_{x,b}) = \Delta_{x,b} \in t(x)(b)$

• if $a \neq b$ and $t(x)(b) = \star$, then $r(y)(b) = \star$;

• if $a = b$, then $r(y)(b) = \Delta''$, and $\mathcal{D}(\text{corr})(\Delta'') = \Delta'$, with $\Delta' \in \text{conv}(t(x)(a))$.

To conclude the proof we only need to show that (1) and (2) hold. The former is trivially satisfied by definition of corr. For (2), we derive:

$$
\begin{align*}
\mathcal{D}(\text{corr}+1)(\text{reach}_{\mathcal{R}}(y)(aw')) &= \mathcal{D}(\text{corr}+1)\left(\sum_{y_{x'} \in \text{supp}(\Delta'')} (\Delta''(y_{x'}) \cdot \text{reach}_{\mathcal{R}}(y_{x'})(w'))\right) \\
&= \mathcal{D}(\text{corr}+1)\left(\sum_{x' \in \text{supp}(\Delta')} (\Delta'(x') \cdot \text{reach}_{\mathcal{R}}(y_{x'})(w'))\right) \\
&= \sum_{x' \in \text{supp}(\Delta')} \Delta'(x') \cdot (\mathcal{D}(\text{corr}+1)(\text{reach}_{\mathcal{R}}(y_{x'})(w')) \\
&= \sum_{x' \in \text{supp}(\Delta')} \Delta'(x') \cdot \Delta'_{x'} \\
&= \Delta \Box
\end{align*}
$$

Proof of Theorem 8.4. Before starting with the actual proof, we need the following elemen-
tary observation: for all $f: X \to Y$ and $\Delta \in \mathcal{D}(X+1)$, it holds that

$$
o^{\#}(\mathcal{D}(f+1)(\Delta)) = o^{\#}(\Delta), \quad (8.1)
$$

namely, the total mass is preserved by applying $\mathcal{D}(f+1)$.

Now, suppose that $[\eta(x)](w) = [p, q]$ for some $p, q \in [0, 1]$ with $p \le q$. By Proposition 8.9, it holds that $\bar{o}^{\#}(\text{reach}(x)(w)) = [p, q]$. By definition of $\bar{o}^{\#}$ there exists $\Delta_{min}, \Delta_{max} \in \text{reach}(x)(w)$ such that the total mass of $\Delta_{min} = p$, the total mass of $\Delta_{max} = q$ and for an arbitrary $\Delta \in \text{reach}(x)$, its total mass is in between $p$ and $q$. In other words,

(a) $o^{\#}(\Delta_{min}) = p$,

(b) $o^{\#}(\Delta_{max}) = q$ and

(c) $p \le o^{\#}(\Delta) \le q$ for all $\Delta \in \text{reach}(x)$.

By Proposition 8.10, for all resolutions $\mathcal{R}$, states $y$ such that $\text{corr}(y) = x$, and distributions $\Delta'$ such that $\text{reach}_{\mathcal{R}}(y)(w) = \Delta'$, one has that $\mathcal{D}(\text{corr}+1)(\Delta') \in \text{reach}(x)(w)$. By (c), $p \le o^{\#}(\mathcal{D}(\text{corr}+1)(\Delta')) \le q$ and, by (8.1), $p \le o^{\#}(\Delta') \le q$. This means $p \le o^{\#}(\text{reach}_{\mathcal{R}}(y)(w)) \le q$ that, by Lemma 8.6, coincides with $p \le \text{prob}_{\mathcal{R}}(y)(w) \le q$. This proves that $[\llcorner x \rrcorner](w) \ge p$ and $[\llcorner x \rrcorner](w) \le q$.

We now prove that $[\llcorner x \rrcorner](w) \le p$; the proof for $[\llcorner x \rrcorner](w) \ge q$ is analogous.

By Proposition 8.11, there exist resolutions $\mathcal{R}$, a state $y$ and a distribution $\Delta''$ such that

(d) $\text{corr}(y) = x$,

(e) $\mathcal{D}(\text{corr}+1)(\Delta'') = \Delta_{\text{min}}$,

(f) $\text{reach}_{\mathcal{R}}(y)(w) = \Delta''$.
By (e) and (8.1), one immediately has that $o^{\#}(\Delta'') = o^{\#}(\Delta_{min}) = p$. By (f), the latter means that $o^{\#}(\mathrm{reach}_{\mathcal{R}}(y)(w)) = p$ that, by Lemma 8.6, allows to conclude that $\mathrm{prob}_{\mathcal{R}}(y)(w) = p$. This proves that $\llbracket x \rrbracket(w) \le p$. $\square$

**Proof of Corollary 8.5.** Consider the monad morphism $q^B: T_{\mathcal{P}CS} \Rightarrow T_{\mathcal{CSB}}$ quotienting $T_{\mathcal{P}CS}$ by (B) (see Section 7), and let $\eta^B, \mu^B$ respectively denote the unit and multiplication of the monad $T_{\mathcal{CSB}}$. Following Remark 7.3 (by Theorem 6.8.1) we have

$$ \llbracket \cdot \rrbracket_B \circ \eta^B = \llbracket \cdot \rrbracket_{B'} \circ \eta $$

where $\llbracket \cdot \rrbracket_{B'}: T_{\mathcal{P}CS}X \to T_{\mathcal{CSB}}1^{A^*}$ is the semantic map induced by the determinisation of $\langle \bar{o}_B, \bar{t} \rangle: X \to T_{\mathcal{CSB}}1 \times (T_{\mathcal{P}CS}X)^A$ using the algebra $\mu_1^B \circ q_1^B: T_{\mathcal{P}CS}T_{\mathcal{CSB}}1 \to T_{\mathcal{CSB}}1$. The monad map $q^B: T_{\mathcal{P}CS} \Rightarrow T_{\mathcal{CSB}}$ gives a $T_{\mathcal{P}CS}$-algebra morphism $q_1^B: (T_{\mathcal{P}CS}1, \mu_1) \to (T_{\mathcal{CSB}}1, \mu_1^B \circ q_1^B)$. By Theorem 6.8.2 we have

$$ \llbracket \cdot \rrbracket_{B'} = q_1^{BA^*} \circ \llbracket \cdot \rrbracket. $$

Hence, we derive

$$ \llbracket \cdot \rrbracket_B \circ \eta^B = q_1^{BA^*} \circ \llbracket \cdot \rrbracket \circ \eta. $$

For an interval $[p, q]$, $q_1^B([p, q]) = q$. Then by Theorem 8.4 we conclude

$$ \begin{align*} (q_1^{BA^*} \circ \llbracket \eta(x) \rrbracket)(w) &= q_1^B(\llbracket \eta(x) \rrbracket(w)) \\ &= q_1^B(\llbracket \llbracket x \rrbracket(w), \llbracket x \rrbracket(w) \rrbracket) \\ &= \llbracket x \rrbracket(w). \end{align*} $$

To prove that $\llbracket \eta(\cdot) \rrbracket_T = \llbracket \cdot \rrbracket$ we proceed in the same way, but taking the monad morphism $q^T: T_{\mathcal{P}CS} \Rightarrow T_{\mathcal{CSJ}}$ quotienting $T_{\mathcal{P}CS}$ by (T). $\square$

**8.2. Coincidence with randomized $\sqcup$-trace equivalence.** Let $t: X \to (\mathcal{P}\mathcal{D}X)^A$ be an NPLTS. A fully probabilistic resolution for $t$ is a triple $\mathcal{R} = (Y, \mathrm{corr}, r)$ such that $Y$ is a set, $\mathrm{corr}: Y \to X$, and $r: Y \to (A \times \mathcal{D}Y) + 1$ such that for every $y \in Y$ and $a \in A$:
if $r(y) = \langle a, \Delta \rangle$ then $\mathcal{D}(\mathrm{corr})(\Delta) \in \mathrm{conv}(t(\mathrm{corr}(y))(a))$.

While resolutions resolve only internal nondeterminism, fully probabilistic resolutions resolve both internal and external nondeterminism. Indeed, in a resolution a state can perform transitions with different labels, while in a fully probabilistic resolution a state can perform at most one transition. Moreover, a state $y$ in a fully probabilistic resolutions might not perform any transition (i.e., $r(y) = \star$), even if the corresponding state $\mathrm{corr}(y)$ may perform a transition (i.e., $t(\mathrm{corr}(y))(a) \neq \star$ for some $a$).

**Example 8.12.** As in Example 8.2, consider the NPLTS on the left of Figure 1. The resolution $\mathcal{R}_1$ in Figure 6 is a fully probabilistic resolution, while $\mathcal{R}_2$ and $\mathcal{R}_3$ are not, since $x_2$ is allowed to perform more than one transition, even if labelled by different actions.

In Figure 7, we show three examples of fully probabilistic resolutions of the same NPLTS. Note that neither of them is a resolution. In $\mathcal{R}_1$, state $x_1$ does not satisfy the first clause of the definition of resolution, since $x_1$ does not move while its corresponding state in the original NPLTS does. In $\mathcal{R}_2$ and $\mathcal{R}_3$, state $x_2$ respectively only performs a b-labelled
<figure><img src="image_31.png" /><figcaption>Figure 7: Fully probabilistic resolutions ($\mathcal{R}_1, \mathcal{R}_2, \mathcal{R}_3$, from left to right)</figcaption></figure>

transition and only performs a c-labelled transition. In a resolution, it should perform both.

As for resolutions, we can define $prob_{\mathcal{R}}: Y \to [0, 1]^{A^*}$ for $\mathcal{R} = (Y, \text{corr}, r)$ a fully probabilistic resolution inductively for all $y \in Y$ and all $w \in A^*$ as

$$ \text{prob}_{\mathcal{R}}(y)(\varepsilon) = 1; $$

$$ \text{prob}_{\mathcal{R}}(y)(aw) = \begin{cases} \sum_{y' \in \text{supp}(\Delta)} \Delta(y') \cdot \text{prob}_{\mathcal{R}}(y')(w) & \text{if } r(y) = \langle a, \Delta \rangle, \\ 0 & \text{otherwise.} \end{cases} $$

Given an NPLTS $(X, t)$, we define for $x \in X$ and $w \in A^*$:

$$ \llbracket x \rrbracket_{fp}(w) = \llbracket \{\text{prob}_{\mathcal{R}}(y)(w) \mid \mathcal{R} = (Y, \text{corr}, r) \text{ is a fully probabilistic resolution of } (X, t) \text{ and } \text{corr}(y) = x \}. $$

In [Cas18] (following [BDL14b, BDL14a]), two states $x$ and $y$ are defined to be *ran-domized* $\sqcup$-trace equivalent whenever $\llbracket x \rrbracket_{fp}(w) = \llbracket y \rrbracket_{fp}(w)$, for all $w \in A^*$.<fnref n="7" /> The following proposition guarantees that such equivalence coincides with $\equiv_B$.

**Proposition 8.13.** Let $(X, t)$ be an NPLTS. For all $x \in X$ and $w \in A^*$, it holds that $\llbracket x \rrbracket_B(w) = \llbracket x \rrbracket(w) = \llbracket x \rrbracket_{fp}(w)$.

*Proof.* We first prove that $\llbracket x \rrbracket(w) \le \llbracket x \rrbracket_{fp}(w)$.

Let $\mathcal{R} = (Y, \text{corr}, r)$ be a resolution of $(X, t)$, $x \in X$, and $w \in A^*$. Let $y \in Y$ such that $\text{corr}(y) = x$. We show that there exists a fully probabilistic resolution $\mathcal{R}'$ of $(X, t)$ with a state $z$ such that $z$ is mapped by the correspondence function of $\mathcal{R}'$ to $x$ and such that $\text{prob}_{\mathcal{R}}(y)(w) = \text{prob}_{\mathcal{R}'}(z)(w)$.

We define $\mathcal{R}' = (Y \times A^*, \text{corr}', r')$ as follows. The correspondece function $\text{corr}'$: $Y \times A^* \to Y$ is $\text{corr} \circ \pi_1$, namely $\text{corr}'(y, w') = \text{corr}(y)$ for all $w' \in A^*$. To define $r'$, we use the notation $\Delta_{w'} \in \mathcal{D}(Y \times A^*)$ to denote, for all $\Delta \in \mathcal{D}(Y)$ and $w' \in A^*$, the distribution over $Y \times A^*$ given as

$$ \Delta_{w'}(y, w'') = \begin{cases} \Delta(y) & \text{if } w' = w'', \\ 0 & \text{otherwise.} \end{cases} $$

<footnote n="7">⁷Actually, [Cas18, BDL14b, BDL14a] use a notion of resolution which is equal to our fully-probabilistic resolution modulo a tiny modification due to a mistake in [BDL14b, BDL14a], as confirmed by the authors in a personal communication.</footnote>
Now $r': Y \times A^* \to (A \times \mathcal{D}(Y \times A^*)) + 1$ is defined as:

$$ 
\begin{aligned}
r'(y, \epsilon) &= \star \\
r'(y, aw') &= \begin{cases} \langle a, \Delta_{w'} \rangle & \text{if } r(y)(a) = \Delta \neq \star \\ \star & \text{otherwise.} \end{cases}
\end{aligned}
$$

First, it is necessary to observe that $\mathcal{R}'$ is indeed a fully probabilistic system, that is, for every state there is at most one transition that can be performed. Indeed, by taking as set of states of $\mathcal{R}'$ the set $Y \times A^*$, we guarantee that despite a state $y$ in $\mathcal{R}$ might perform different transitions reaching distributions over states (one for each label), only one of these transitions is actually performed by a corresponding state $(y, aw')$ in $\mathcal{R}'$, namely the transition with label $a$. This allows us to move from a (reactive) resolution $\mathcal{R}$ to a fully probabilistic resolution $\mathcal{R}'$, while preserving the probability of performing traces. As we will prove below, for all $w$ and $y$ it holds $\text{prob}_{\mathcal{R}}(y)(w) = \text{prob}_{\mathcal{R}'}(y, w)(w)$. To illustrate this with an example, suppose the resolution $\mathcal{R}$ is the RPLTS with two states $y, y'$ and with $r(y)(a) = \delta_y$ and $r(y)(b) = \delta_{y'}$. Take the trace $ab$, for which we have $\text{prob}_{\mathcal{R}}(y)(ab) = 1$. Then in $\mathcal{R}'$ we have $r'(y, ab) = \langle a, \delta_{(y,b)} \rangle$ and $r'(y, b) = \langle b, \delta_{(y',\epsilon)} \rangle$, which gives $\text{prob}_{\mathcal{R}'}(y, ab)(ab) = 1$.

We proceed by proving that $\mathcal{R}'$ is a fully probabilistic resolution of $(X, t)$. Suppose that $r'(y, w') \neq \star$. Then $w' = aw''$, and $r'(y, w') = \langle a, \Delta_{w''} \rangle$ with $\Delta = r(y)(a)$. Hence, $\mathcal{D}(\text{corr}')(\Delta_{w''}) = \mathcal{D}(\text{corr})(\Delta)$. Since $\mathcal{R}$ is a resolution, $\mathcal{D}(\text{corr})(\Delta) \in \text{conv}(t(x)(a))$ and therefore $\mathcal{R}'$ is a fully probabilistic resolution.

We now prove that for all $w' \in A^*$ and for all $y \in Y$, it holds that $\text{prob}_{\mathcal{R}}(y)(w') = \text{prob}_{\mathcal{R}'}(y, w')(w')$. The proof goes by induction on $w'$.

If $w' = \epsilon$ then, $\text{prob}_{\mathcal{R}}(y)(\epsilon) = 1 = \text{prob}_{\mathcal{R}'}(y, \epsilon)(\epsilon)$.

If $w' = aw''$ and $r(y)(a) = \star$, then $r'(y, w') = \star$ and $\text{prob}_{\mathcal{R}'}(y, w')(w') = 0 = \text{prob}_{\mathcal{R}}(y)(w')$.

If $w' = aw''$ and $r(y)(a) = \Delta \neq \star$, then $r'(y, aw'') = \langle a, \Delta_{w''} \rangle$ and

$$ 
\begin{aligned}
\text{prob}_{\mathcal{R}}(y)(w') &= \sum_{y' \in \text{supp}(\Delta)} \Delta(y') \cdot \text{prob}_{\mathcal{R}}(y')(w'') \\
&= \sum_{y' \in \text{supp}(\Delta)} \Delta(y') \cdot \text{prob}_{\mathcal{R}'}(y', w'')(w'') \\
&= \sum_{(y', w'') \in \text{supp}(\Delta_{w''})} \Delta_{w''}(y', w'') \cdot \text{prob}_{\mathcal{R}'}(y', w'')(w'') \\
&= \text{prob}_{\mathcal{R}'}(y, aw'')(aw'')
\end{aligned}
$$

Hence, $\text{prob}_{\mathcal{R}}(y)(w) = \text{prob}_{\mathcal{R}'}(y, w)(w)$, with $\text{corr}(y) = \text{corr}'(y, w) = x$.

We now prove that $\llbracket x \rrbracket(w) \geq \llbracket x \rrbracket_{fp}(w)$.

Let $\mathcal{R} = (Y, \text{corr}, r)$ be a fully probabilistic resolution of $(X, t)$, $x \in X$, and $w \in A^*$. Let $\text{corr}(y) = x$. We show that there exists a resolution $\mathcal{R}' = (Y', \text{corr}', r')$ of $(X, t)$ with a state $z$ such that $\text{corr}'(z) = x$ and $\text{prob}_{\mathcal{R}}(y)(w) \leq \text{prob}_{\mathcal{R}'}(z)(w)$. We define $\mathcal{R}' = (Y', \text{corr}', r')$ as follows:

* $Y' = Y + X$ is the (disjoint) union of $Y$ and $X$
• $\mathrm{corr}' = \mathrm{corr} + \mathrm{id}_X$ that is for all $y' \in Y'$

$$ \mathrm{corr}'(y') = \begin{cases} \mathrm{corr}(y') & \text{if } y' \in Y; \\ \mathrm{id}_X(y') & \text{if } y' \in X. \end{cases} $$

• $r' : Y' \to (\mathcal{D}(Y') + 1)^A$ is defined as:

$$ r'(y')(a) = \begin{cases} \star & \text{if } t(\mathrm{corr}'(y'))(a) = \star \\ \Delta & \text{if } y' \in Y \text{ and } r(y') = \langle a, \Delta \rangle \\ \Delta_{\mathrm{corr}'(y'),a} & \text{otherwise} \end{cases} $$

where $\Delta_{x,a}$ are defined like in the base case of the proof of Proposition 8.11 (namely, an arbitrary choice amongst the distributions in $t(x)(a)$).

We prove that $\mathcal{R}'$ is a resolution. For elements $y' \in X$ the conditions of Definition 8.1 are trivially satisfied (see the analogous construction used in the base case in the proof of Proposition 8.11). Suppose $y' \in Y$.

(1) By definition, $r'(y')(a) = \star$ iff $t(\mathrm{corr}'(y'))(a) = \star$.

(2) If $r'(y')(a) \neq \star$, then we are either in the second or in the third case of the definition of $r'$. If we are in the second case, $r'(y')(a) = \Delta$ with $r(y') = \langle a, \Delta \rangle$. Since $\Delta \in \mathcal{D}Y$ we have $\mathcal{D}(\mathrm{corr}')(\Delta) = \mathcal{D}(\mathrm{corr})(\Delta)$, and by the definition of fully probabilistic resolution, it holds that $\mathcal{D}(\mathrm{corr})(\Delta) \in \mathrm{conv}(t(\mathrm{corr}(y'))(a))$. Therefore $\mathcal{D}(\mathrm{corr}')(\Delta) \in \mathrm{conv}(t(\mathrm{corr}'(y'))(a))$. If we are in the third case, we have $r'(y')(a) = \Delta_{\mathrm{corr}'(y'),a}$, with $\Delta_{\mathrm{corr}'(y'),a} \in t(\mathrm{corr}'(y'))(a)$. By definition of $\mathrm{corr}'$, $\mathcal{D}(\mathrm{corr}')(\Delta_{\mathrm{corr}'(y'),a}) = \Delta_{\mathrm{corr}'(y'),a}$. Therefore $\mathcal{D}(\mathrm{corr}')(\Delta_{\mathrm{corr}'(y'),a}) \in \mathrm{conv}(t(\mathrm{corr}'(y'))(a))$.

We conclude by showing that for all $y \in Y$ and for all $w'$, $\mathrm{prob}_{\mathcal{R}}(y, w') \le \mathrm{prob}_{\mathcal{R}'}(y, w')$. The proof goes by induction on $w'$. The case $w' = \epsilon$ is trivial, since $\mathrm{prob}_{\mathcal{R}}(y, \epsilon) = 1 = \mathrm{prob}_{\mathcal{R}'}(y, \epsilon)$. For the inductive case, take $w' = aw''$. Suppose $r(y) = \langle a, \Delta \rangle$. Then, by definition of $r'$, $r'(y)(a) = \Delta$, and

$$ \begin{align*} \mathrm{prob}_{\mathcal{R}}(y)(aw'') &= \sum_{y' \in \mathrm{supp}(\Delta)} \Delta(y') \cdot \mathrm{prob}_{\mathcal{R}}(y')(w'') \\ &\le \sum_{y' \in \mathrm{supp}(\Delta)} \Delta(y') \cdot \mathrm{prob}_{\mathcal{R}'}(y')(w'') \quad (\text{by IH}) \\ &= \mathrm{prob}_{\mathcal{R}'}(y)(aw'') \end{align*} $$

Now suppose that $r(y) \neq \langle a, \Delta \rangle$. Then $r(y) = \star$ and, by definition of $\mathrm{prob}_{\mathcal{R}}$, $\mathrm{prob}_{\mathcal{R}}(y)(aw'') = 0$, so there is nothing to prove.

Hence, $\mathrm{prob}_{\mathcal{R}}(y)(w) \le \mathrm{prob}_{\mathcal{R}'}(y)(w)$, with $\mathrm{corr}(y) = \mathrm{corr}'(y) = x$. $\square$

**Remark 8.14.** The correspondence in Proposition 8.13 does not hold when infima are considered, instead of suprema. Indeed define $[\llcorner x\rrcorner]_{fp}(w)$ as expected, namely, by replacing $\llcorner$ with $\lceil$ in $[\llcorner x\rrcorner]_{fp}(w)$. Then for any state $x$ of an arbitrary NPLTS it holds that $[\llcorner x\rrcorner]_{fp}(w) = 0$ for all $w \neq \varepsilon$. To see this, observe that $\mathcal{R}' = (\{y\}, \mathrm{corr}', r')$ with $\mathrm{corr}'(y) = x$ and $r'(y) = \star$ is always a fully probabilistic resolution, and that $\mathrm{prob}_{\mathcal{R}'}(y)(w) = 0$.

To avoid this problem, one typically modifies the definition of $[\llcorner \cdot \rrcorner]_{fp}$ by restricting only to those fully probabilistic resolutions that can perform a certain trace (see e.g. [BDL14b, BDL14a]). Instead, with our notion of resolution based on RPLTSs (Definition 8.1), this problem does not arise and the definition of $[\llcorner \cdot \rrcorner]$ is totally analogous to the one of $[\llcorner \cdot \rrcorner]$.
**Why may, must, may-must? Trace equivalences as testing equivalences** The notion of resolution is at the basis not just of the definitions of trace equivalences for NPLTS investigated in the literature, but also of testing equivalences for nondeterministic and probabilistic processes [YL92, JHSY94, DGH$^+$07, DGHM09], extending the theory of testing equivalences for purely nondeterministic processes [DH84] (see Remark 6.15). In testing equivalences for nondeterministic and probabilistic processes, we say that $x, y$ are may testing equivalent if, for every test, they have the same greatest probabilities of passing the test, with respect to any resolution $\mathcal{R}$ of the system resulting from the interaction between the test and the NPLTS. Analogously, $x, y$ are must testing equivalent if the smallest probabilities coincide, and the may-must testing equivalence requires both the greatest and the smallest probabilities to coincide.

Now, take tests to be finite traces, and the probability of passing a given test in a resolution as the probability of performing the trace in the resolution. Then it becomes clear, by the correspondence between the local and the global view proven in Theorem 8.4, that each of our three trace equivalences indeed coincides with the corresponding testing equivalence, when tests are finite traces.

## 9. CONCLUSION AND FUTURE WORK

We developed an algebra-and-coalgebra-based trace theory for systems with nondeterminism and probability, that covers intricate trace semantics from the literature. The abstract approach sheds light on all choices and leaves no space for ad-hoc solutions.

Although the combination of nondeterminism and probability has been posing challenges to abstract approaches, this new algebraic theory of traces for NPLTS shows that it can be dealt with in a smooth and uniform way.

In [Jac08], Jacobs leaves open the question of whether the semantics that he obtains by exploiting the Kleisli traces [HJS07] for the monad *C* coincides with some scheduler based semantics. We would like to answer that such semantics corresponds to the may-must trace equivalence by our results and the correspondence between Kleisli traces and generalised determinisation studied in [JSS15]. However, we cannot directly derive this: for technical reasons (namely, the absence of a bottom element in the Kleisli category of *C*), Jacobs has to hack the general framework in [HJS07] and therefore the correspondence does not follow from known results. Providing an answer to this interesting question is left as future work.

## REFERENCES

[Bar04] F. Bartels. *On generalised coinduction and probabilistic specification formats: distributive laws in coalgebraic modelling*. PhD thesis, Vrije Universiteit, Amsterdam, 2004.

[BBC$^+$16] F. Bonchi, M.M. Bonsangue, G. Caltais, J. Rutten, and A. Silva. A coalgebraic view on decorated traces. *Mathematical Structures in Computer Science*, 26(7):1234–1268, 2016. doi: 10.1017/S0960129514000449.

[BDL14a] M. Bernardo, R. De Nicola, and M. Loreti. Relating strong behavioral equivalences for processes with nondeterminism and probabilities. *Theoretical Computer Science*, 2014.

[BDL14b] M. Bernardo, R. De Nicola, and M. Loreti. Revisiting trace and testing equivalences for non-deterministic and probabilistic processes. *Logical Methods in Computer Science*, 10(1:16):1–42, 2014.

[BK08] C. Baier and J.P. Katoen. *Principles of model checking*. MIT Press, 2008.

[BP13] F. Bonchi and D. Pous. Checking NFA equivalence with bisimulations up to congruence. In *Proc. POPL 2013*, pages 457–468. ACM, 2013.
[BPPR17] F. Bonchi, D. Petrisan, D. Pous, and J. Rot. A general account of coinduction up-to. *Acta Informatica*, 54(2):127-190, 2017. doi:10.1007/s00236-016-0271-4.

[Brz64] J.A. Brzozowski. Derivatives of regular expressions. *Journal of the ACM*, pages 481–494, 1964.

[BSS17] F. Bonchi, A. Silva, and A. Sokolova. The Power of Convex Algebras. In *Proc. CONCUR 2017*, volume 85, pages 23:1–23:18. LIPIcs, 2017. doi:10.4230/LIPIcs.CONCUR.2017.23.

[BSV04] F. Bartels, A. Sokolova, and E.P. de Vink. A hierarchy of probabilistic system types. *Theoretical Computer Science*, 327:3–22, 2004.

[BSV21] Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. Presenting convex sets of probability distributions by convex semilattices and unique bases ((co)algebraic pearls). In *Proc. CALCO 2021*, volume 211, pages 11:1–11:18. LIPIcs, 2021. doi:10.4230/LIPIcs.CALCO.2021.11.

[Cas18] V. Castiglioni. Trace and testing metrics on nondeterministic probabilistic processes. In *Proc. Express/SOS 2018.*, pages 19–36, 2018. doi:10.4204/EPTCS.276.4.

[CPP09] P.S. Castro, P. Panangaden, and D. Precup. Equivalence relations in fully and partially observable markov decision processes. In *Proc. IJCAI 2009*, pages 1653–1658, 2009.

[DGH+07] Y. Deng, R.J. van Glabbeek, M. Hennessy, C. Morgan, and C. Zhang. Characterising testing preorders for finite probabilistic processes. In *Proc. LICS 2007*, pages 313–325. IEEE-CS Press, 2007.

[DGHM09] Y. Deng, R.J. van Glabbeek, M. Hennessy, and C. Morgan. Testing finitary probabilistic processes. In *Proc. CONCUR 2009*, volume 5710 of LNCS, pages 274–288. Springer, 2009.

[DH84] R. De Nicola and M. Hennessy. Testing equivalences for processes. *Theoretical Computer Science*, 34:83–133, 1984.

[DJKV17] C. Dehnert, S. Junges, J.P. Katoen, and M. Volk. A storm is coming: A modern probabilistic model checker. In *Proc. CAV 2017*, volume 10427 of LNCS, pages 592–600, 2017.

[Dob06] E.E. Doberkat. Eilenberg-Moore algebras for stochastic relations. *Information and Computation*, 204(12):1756-1781, 2006. URL: http://dx.doi.org/10.1016/j.ic.2006.09.001, doi:10.1016/j.ic.2006.09.001.

[Dob08] E.E. Doberkat. Erratum and addendum: Eilenberg-Moore algebras for stochastic relations [mr2277336]. *Information and Computation*, 206(12):1476-1484, 2008. URL: http://dx.doi.org/10.1016/j.ic.2008.08.002, doi:10.1016/j.ic.2008.08.002.

[DP97] D.Turi and G. D. Plotkin. Towards a mathematical operational semantics. In *Proc. LICS 1997*, pages 280–291, 1997. doi:10.1109/LICS.1997.614955.

[DPS18] F. Dahlqvist, L. Parlant, and A. Silva. Layer by layer - combining monads. In *Proc. ICTAC 2018*, pages 153–172, 2018. doi:10.1007/978-3-030-02508-3\_9.

[FZ14] Y. Feng and L. Zhang. When equivalence and bisimulation join forces in probabilistic automata. In *Cliff Jones, Pekka Pihlajasaari, and Jun Sun, editors, Proc. FM 2014*, pages 247–262, Cham, 2014. Springer International Publishing.

[Gla01] R.J. van Glabbeek. The linear time - branching time spectrum i. the semantics of concrete, sequential processes. In J. A. Bergstra, A. Ponse, and S.A. Smolka, editors, *Handbook of Process Algebra*, pages 3–99. Elsevier, Amsterdam, 2001.

[Han91] H. A. Hansson. *Time and probability in formal design of distributed systems*. PhD thesis, Uppsala University, 1991.

[HJS07] I. Hasuo, B. Jacobs, and A. Sokolova. Generic trace semantics via coinduction. *Logical Methods in Computer Science*, 3(4), 2007. doi:10.2168/LMCS-3(4:11)2007.

[HKK14] H. Hermanns, J. Krcál, and J. Kretínský. Probabilistic bisimulation: Naturally on distributions. In *Proc. CONCUR 2014*, volume 8704 of LNCS, pages 249–265, 2014.

[HKSH17] C. Heunen, O. Kammar, S. Staton, and H.Yang. A convenient category for higher-order probability theory. *CoRR*, abs/1701.02547, 2017. URL: http://arxiv.org/abs/1701.02547.

[HPP02] M. Hyland, G.D. Plotkin, and J. Power. Combining computational effects: Commutativity and sum. In *Foundations of Information Technology in the Era of Network and Mobile Computing*, pages 474–484. Springer, 2002.

[HPS+11] H. Hermanns, A. Parma, R. Segala, B. Wachter, and L. Zhang. Probabilistic logical characterization. *Information and Computation*, 209(2):154–172, 2011.

[Jac08] B. Jacobs. Coalgebraic trace semantics for combined possibilitistic and probabilistic systems. *Electronic Notes in Theoretical Computer Science*, 203(5):131–152, 2008.
[Jac10] B. Jacobs. Convexity, duality and effects. In *Theoretical computer science*, volume 323 of *IFIP Adv. Inf. Commun. Technol.*, pages 1–19. Springer, Berlin, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15240-5_1, doi:10.1007/978-3-642-15240-5\_1.

[Jac16] B. Jacobs. *Introduction to Coalgebra: Towards Mathematics of States and Observation*. Cambridge University Press, 2016.

[J.G08] J.G.-Larrecq. Prevision domains and convex powercones. In *Proc. FOSSACS 2008*, pages 318–333. LNCS 4962, 2008. doi:10.1007/978-3-540-78499-9\_23.

[JHSY94] B. Jonsson, C. Ho-Stuart, and W. Yi. Testing and refinement for nondeterministic and probabilistic processes. In *Proc. FTRTFT 1994*, volume 863 of LNCS, pages 418–430. Springer, 1994.

[JSS15] B. Jacobs, A. Silva, and A. Sokolova. Trace semantics via determinization. *Journal of Computer and System Sciences*, 81(5):859–879, 2015.

[KLC98] L.P. Kaelbling, M.L. Littman, and A.R. Cassandra. Planning and Acting in Partially Observable Stochastic Domains. *Artificial Intelligence*, 1998.

[Kli11] B. Klin. Bialgebras for structural operational semantics: An introduction. *Theoretical Computer Science*, 412(38):5043–5069, 2011. doi:10.1016/j.tcs.2011.03.023.

[KNP02] M. Z. Kwiatkowska, G. Norman, and D. Parker. Prism: Probabilistic symbolic model checker. In *Proc. TOOLS 2002*, pages 200–204. LNCS 2324, 2002.

[KP17] K. Keimel and G.D. Plotkin. Mixed powerdomains for probability and nondeterminism. *Logical Methods in Computer Science*, 13(1), 2017. doi:10.23638/LMCS-13(1:2)2017.

[KR16] B. Klin and J. Rot. Coalgebraic trace semantics via forgetful logics. *Logical Methods in Computer Science*, 12(4), 2016. doi:10.2168/LMCS-12(4:10)2016.

[Kur00] A. Kurz. *Logics for Coalgebras and Applications to Computer Science*. PhD thesis, Ludwig-Maximilians-Universität München, 2000.

[LS91] K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. *Information and Computation*, 94:1–28, 1991.

[Mac71] S. MacLane. *Categories for the working mathematician*. Springer-Verlag, 1971.

[Mil89] R. Milner. *Communication and Concurrency*. Prentice Hall, 1989.

[Mio14] M. Mio. Upper-expectation bisimilarity and lukasiewicz $\mu$-calculus. In *Proc. FOSSACS 2014*, volume 8412 of LNCS, pages 335–350, 2014.

[Mis00] M.W. Mislove. Nondeterminism and probabilistic choice: Obeying the laws. In *Proc. CONCUR 2000*, pages 350–364. LNCS 1877, 2000. doi:10.1007/3-540-44618-4\_26.

[MOW03] M. Mislove, J. Ouaknine, and J. Worrell. Axioms for probability and nondeterminism. In *Proc. EXPRESS 2003*, volume 96 of Electronic Notes in Theoretical Computer Science, pages 7–28. Elsevier, 2003.

[MSV21] Matteo Mio, Ralph Sarkis, and Valeria Vignudelli. Combining nondeterminism, probability, and termination: Equational and metric reasoning. In *Proc. LICS 2021*, pages 1–14. IEEE, 2021. doi:10.1109/LICS52264.2021.9470717.

[MV20] Matteo Mio and Valeria Vignudelli. Monads and quantitative equational theories for nondeterminism and probability. In *Proc. CONCUR 2020*, volume 171 of LIPIcs, pages 28:1–28:18, 2020. doi:10.4230/LIPIcs.CONCUR.2020.28.

[Pou07] D. Pous. Complete lattices and up-to techniques. In *Proc. APLAS 2007*, volume 4807, pages 351–366, 2007. URL: http://dx.doi.org/10.1007/978-3-540-76637-7\_24.

[PR95] Dieter Pumplün and Helmut Röhrl. Convexity theories. IV. Klein-Hilbert parts in convex modules. *Applied Categorical Structures*, 3(2):173–200, 1995. URL: http://dx.doi.org/10.1007/BF00877635, doi:10.1007/BF00877635.

[PS12] D. Pous and D. Sangiorgi. Enhancements of the bisimulation proof method. In Davide Sangiorgi and Jan Rutten, editors, *Advanced Topics in Bisimulation and Coinduction*. Cambridge University Press, 2012.

[Rab63] M.O. Rabin. Probabilistic automata. *Information and Control*, 6:230–245, 1963.

[RN09] S. Russell and P. Norvig. *Artificial Intelligence: A Modern Approach*. Prentice Hall, 2009.

[Rut00] J.J.M.M. Rutten. Universal coalgebra: A theory of systems. *Theoretical Computer Science*, 249:3–80, 2000.

[Ś74] T. Świrszcz. Monadic functors and convexity. *Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys.*, 22:39–42, 1974.
[San98] D. Sangiorgi. On the bisimulation proof method. *Mathematical Structures in Computer Science*, 8(5):447–479, 1998.

[SBBR10] A. Silva, F. Bonchi, M. Bonsangue, and J. Rutten. Generalizing the powerset construction, coalgebraically. In *Proc. FSTTCS 2010*, volume 8 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 272–283, 2010.

[Seg95a] R. Segala. A compositional trace-based semantics for probabilistic automata. In *Proc. CONCUR 1995*, volume 962 of LNCS, pages 234–248. Springer, 1995.

[Seg95b] R. Segala. *Modeling and verification of randomized distributed real-time systems*. PhD thesis, MIT, 1995.

[Sem73] Zbigniew Semadeni. *Monads and their Eilenberg-Moore algebras in functional analysis*. Queen's University, Kingston, Ont., 1973.

[SL94] R. Segala and N.A. Lynch. Probabilistic simulations for probabilistic processes. In *Proc. CONCUR 1994*, pages 481–496. LNCS 836, 1994.

[SL95] R. Segala and N. Lynch. Probabilistic simulations for probabilistic processes. *Nordic Journal of Computing*, 2(2):250–273, 1995.

[Sok11] A. Sokolova. Probabilistic systems coalgebraically: A survey. *Theoretical Computer Science*, 412(38):5095–5110, 2011.

[Sta11] S. Staton. Relating coalgebraic notions of bisimulation. *Logical Methods in Computer Science*, 7(1), 2011.

[Sto49] M.H. Stone. Postulates for the barycentric calculus. *Annali di Matematica Pura ed Applicata. Serie Quarta*, 29:25–30, 1949. URL: http://dx.doi.org/10.1007/BF02413910, doi:10.1007/BF02413910.

[SW18] A. Sokolova and H. Woracek. Termination in convex sets of distributions. *Logical Methods in Computer Science*, 14(4), 2018.

[SYW$^+$16] S. Staton, H. Yang, F. Wood, C. Heunen, and O. Kammar. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In *Proc. LICS 2016*, pages 525–534, 2016. URL: http://doi.acm.org/10.1145/2933575.2935313, doi:10.1145/2933575.2935313.

[TKP09] R. Tix, K. Keimel, and G.D. Plotkin. Semantic domains for combining probability and nondeterminism. *Electronic Notes in Theoretical Computer Science*, 222:3–99, 2009. doi:10.1016/j.entcs.2009.01.002.

[Var85] M.Y. Vardi. Automatic verification of probabilistic concurrent finite state programs. In *Proc. FOCS 1985*, pages 327–338. IEEE, 1985.

[Var03] D. Varacca. *Probability, Nondeterminism and Concurrency: Two Denotational Models for Probabilistic Computation*. PhD thesis, Univ. Aarhus, 2003.

[vHHOS18] G. van Heerdt, J. Hsu, J. Ouaknine, and A. Silva. Convex Language Semantics for Nondeterministic Probabilistic Automata. In *Proc. ICTAC 2018*, pages 472–492, 2018.

[VW06] D. Varacca and G. Winskel. Distributing probability over nondeterminism. *Mathematical Structures in Computer Science*, 16(1):87–113, 2006.

[Wol00] U. Wolter. On corelations, cokernels, and coequations. *Electronic Notes in Theoretical Computer Science*, 33, 2000.

[YJZ17] P. Yang, D.N. Jansen, and L. Zhang. Distribution-based bisimulation for labelled markov processes. In *Proc. FORMATS 2017*, pages 170–186, 2017. doi:10.1007/978-3-319-65765-3\_10.

[YL92] W. Yi and K.G. Larsen. Testing probabilistic and nondeterministic processes. In *Proc. PSTV 1992*, pages 47–61. North-Holland, 1992.