A Complete Inference System for Probabilistic Infinite Trace Equivalence

Cîrstea, Corina; Moss, Lawrence S.; Noquez, Victoria; Schmid, Todd; Silva, Alexandra; Sokolova, Ana

doi:10.4230/LIPIcs.CSL.2025.30

A Complete Inference System for Probabilistic Infinite Trace Equivalence

Corina Cîrstea

University of Southampton, UK Lawrence S. Moss

Indiana University, Bloomington, IN, USA Victoria Noquez

Saint Mary’s College of California, Moraga, CA, USA Todd Schmid

Bucknell University, Lewisburg, PA, USA Alexandra Silva

Cornell University, Ithaca, NY, USA Ana Sokolova

Paris Lodron University of Salzburg, Austria

Abstract

We present the first sound and complete axiomatization of infinite trace semantics for generative probabilistic transition systems. Our approach is categorical, and we build on recent results on proper functors over convex sets. At the core of our proof is a characterization of infinite traces as the final coalgebra of a functor over convex algebras. Somewhat surprisingly, our axiomatization of infinite trace semantics coincides with that of finite trace semantics, even though the techniques used in the completeness proof are significantly different.

Keywords and phrases:

Coalgebra, infinite trace, semantics, logic, convex sets

Funding:

Corina Cîrstea: partly supported by the Leverhulme Trust Research Project Grant RPG-2020-232.

Lawrence S. Moss: Lawrence S. Moss was supported by grant #586136 from the Simons Foundation.

Alexandra Silva: ERC grant Autoprobe (no. 101002697). This work was done in part while the author was visiting the Simons Institute for the Theory of Computing.

Copyright and License:

© Corina Cîrstea, Lawrence S. Moss, Victoria Noquez, Todd Schmid, Alexandra Silva, and
Ana Sokolova; licensed under Creative Commons License CC-BY 4.0

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Logic ; Theory of computation

\rightarrow

Formal languages and automata theory

Acknowledgements:

We thank Wojtek Rozowski for insightful discussions on related topics and the anonymous reviewers for helpful suggestions that improved the material presented in the paper. We thank the National Science Foundation and the Simons Laufer Mathematical Sciences Institute for their support of our work.

Funding:

This material is based upon work supported by the National Science Foundation under Grant No. DMS-1928930, while the authors were in residence at the Mathematical Sciences Research Institute in Berkeley, California, during the Summer Research in Mathematics program of 2024.

DOI:

10.4230/LIPIcs.CSL.2025.30

Event:

33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Editors:

Jörg Endrullis and Sylvain Schmitz

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Probabilistic transition systems have been studied in the semantics and verification literature for decades. There are many variants, from the simplest Rabin model [16] to systems that encompass multiple layers of randomized and non-deterministic choice. A good overview of existing systems and an expressiveness hierarchy was provided in [26, 3].

One important class of probabilistic systems are so-called generative probabilistic transition systems (GPTS). These are much like ordinary (nondeterministic) labelled transition systems, but each state is assigned a (sub-)probability distribution over outgoing transitions instead of a set of outgoing transitions. Every state in a GPTS generates a probability distribution of traces. The traces generated can be finite or infinite depending whether the GPTS models explicit termination.

In this paper, we will consider GPTS without explicit termination, also widely known in the literature as Labelled Markov Chains (LMCs), and therefore we are only interested in including infinite traces in the semantics. That is, each state of an LMC we consider generates a probability distribution on infinite traces (a.k.a. streams). The main goal of this paper is to provide an axiomatic characterization of when two states in these LMCs generate the same probability distribution on streams. We provide a syntax and an inference system to reason about distributions on streams generated by a state of an LMC, and prove that the axiomatization is both sound and complete.

Axiomatizing trace distribution semantics is difficult in general, and this is made more challenging by the presence of infinite traces. One of the seminal works on axiomatizing probabilistic behaviours is due to Stark and Smolka [29], but they studied probabilistic bisimilarity (in the sense of [11]), which is a finer equivalence than trace distributions. A decade later [25], Silva and Sokolova showed that adding one extra axiom to Stark and Smolka’s axiomatization of probabilistic bisimilarity was enough to obtain a sound and complete axiomatization of finite trace distribution equivalence. At the core of Silva and Sokolova’s completeness result was the observation that finite trace distribution equivalence coincides with bisimilarity after determinization in the category of convex algebras, algebraic structures that model the closure of convex sets under convex combinations. Stark and Smolka’s result is the probabilistic analogue of an earlier paper of Milner [15], whereas Silva and Sokolova’s is the probabilistic analogue of an earlier paper of Rabinovich [17], where it is shown that a sound and complete axiomatization of trace semantics of labelled transition systems can be obtained from an axiomatization of bisimilarity. All these works, non-deterministic and probabilistic, restrict themselves to finite traces.

To achieve our goal, we use a categorical perspective on the semantics of LMCs. This is in the spirit of [25], but there are crucial technical hurdles to overcome: First, we need to find an endofunctor on a category that models LMCs as coalgebras and allows the derivation of the stream distribution semantics in a canonical way. More specifically, we need to give a coalgebraic characterization of the map that assigns to every state of an LMC the distribution on streams that the state generates. To this end, we carefully craft the endofunctor $G$ on the category $\mathsf{CA}$ of convex algebras and convex algebra homomorphisms in Section 5. Second, we show that our endofunctor satisfies a number of desirable properties that enable a sound and complete axiomatization, including the preservation of pullbacks and properness [14]. Finally, we need to find a suitable syntax for specifying finite LMCs where stream semantics is of interest. Each of these steps pushes the boundaries of existing work on semantics and decidability of trace equivalence for automata, and they require new technical results that form the core contributions of our paper. We briefly describe our contributions below and give an outline of the paper.

$\blacksquare$

In Section 2, we recall basic definitions on labelled Markov chains and their semantics.
$\blacksquare$

In Section 3, we recall the syntax of Stark and Smolka’s process algebra [29] and Silva and Sokolova’s axioms for finite trace equivalence [23], which will form the basis of our inference system and allow us to state our intended soundness and completeness results.
$\blacksquare$

In Section 4, we explain our high-level strategy for proving completeness, which follows the coalgebraic completeness method described in [22] that originates in [8, 24, 13].
$\blacksquare$

In Section 5, we define the endofunctor $G$ , which forms the basis of all of our developments. The functor $G$ is defined on the category $\mathsf{CA}$ of convex algebras and convex algebra homomorphisms (see Definition 4.1), and makes use of an important mass-splitting property that resembles a side condition present in [6]. Crucially, we characterize stream distribution semantics as a final $G$ -coalgebra semantics, via a determinization construction that turns LMCs into $G$ -coalgebras. This construction is interesting in its own right, given its simplicity compared to existing finality-based approaches to infinite trace semantics [9, 5, 6].
$\blacksquare$

In Section 6, we define a $G$ -coalgebra structure on the set of process terms modulo axioms, which endows the terms with an operational semantics. We show that this term coalgebra is universal among the free and finitely generated $G$ -coalgebras by providing unique solutions to finite systems of equations arising from a coalgebra structure.
$\blacksquare$

In Section 7, we conclude our proof of completeness by establishing that $G$ satisfies a property called properness, introduced by Milius in [14]. The proof that $G$ is proper uses a topological characterization of congruences of finitely generated convex algebras due to Sokolova and Woraceck [27].
$\blacksquare$

We conclude with a discussion of related and future work, and the implications of the completeness theorem in Section 8.

Our completeness result is remarkable for two reasons: First and foremost, our axiomatization is precisely the same as Silva and Sokolova’s for finite trace semantics. In other words, both the (finite) trace distribution semantics and the stream distribution semantics give rise to the same valid equations between term expressions. Second, the completeness result uses a novel proof of properness [14, 28] that appears to hinge on the topology of bisimulations between coalgebras over convex algebras. The latter is a significant point of departure from the properness proof method of Sokolova and Woracek [28].

2 Labelled Markov Chains and Stream Semantics

In this section, we briefly recall basic definitions of labelled Markov chains, stream semantics, and the framework of universal coalgebra.

Labelled Markov chains.

Given a set $X$ , define ${\mathcal{D}}(X)$ to be the set of finitely supported probability distributions on $X$ . That is, $\theta\in{\mathcal{D}}(X)$ if and only if $\theta\colon X\to[0,1]$ , $\theta(x)>0$ for finitely many $x\in X$ , and $\theta(X)=\sum_{x\in X}\theta(x)=1$ . Since the support is finite, each $\theta\in{\mathcal{D}}(X)$ can be written in the form $\sum_{i=1}^{n}r_{i}\cdot x_{i}$ such that $r_{i}\in(0,1]$ and $x_{i}\in X$ for each $i\leq n$ . We write $1\cdot x$ for the Dirac delta at $x\in X$ .

For a fixed finite set $A$ of formal symbols called actions, a labelled Markov chain (or LMC) is a pair $(X,\beta)$ consisting of a set $X$ of states and a transition function $\beta\colon X\to{\mathcal{D}}(A\times X)$ . An LMC is said to be finite if it has finitely many states.

One graphical depiction of a finite LMC is the directed graph with a node for each state and a decorated edge $x\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a\mid r}$}}_{\beta}y$ between nodes $x$ and $y$ whenever $\beta(x)(a,y)=r$ with $r>0$ . We typically drop the $\beta$ notation whenever the transition function is clear from context.

Example 2.1.

The LMC $(X,\beta\colon X\to{\mathcal{D}}(A\times X))$ with $A=\{a,b\}$ , $X=\{x,y\}$ , and $\beta(x)(a,y)=\beta(x)(b,x)=\beta(y)(b,x)=\beta(y)(a,y)=0.5$ is depicted in (2.1).

(2.1)

Stream semantics.

A word over a finite alphabet $A$ is a finite sequence $a_{1}\cdots a_{n}$ (written as a juxtaposition) of elements of $A$ . We write $\varepsilon$ for the empty word. A stream is an infinite sequence $(a_{1},a_{2},\dots)$ of elements from $A$ . We write $A^{*}$ for the set of words and $A^{\omega}$ for the set of streams. The set $A^{\omega}$ carries a topology, with basis given by the cylinder sets,

B_{w}=\{(a_{1},\dots,a_{n},\ldots)\mid a_{1}\cdots a_{n}=w\}

where $w\in A^{*}$ is a word. In the notation above, $B_{\varepsilon}=A^{\omega}$ , as every stream begins with $\varepsilon$ .

Recall that a Borel set is an element of the $\sigma$ -algebra generated by the open sets of a topological space, a Borel measure is a measure defined on the Borel sets, and a Borel probability distribution is a Borel measure with total probability $1$ [19].

Definition 2.2.

A stream distribution is a Borel probability distribution on the space $A^{\omega}$ . The set of all stream distributions on $A^{\omega}$ is written $\text{\sf Prob}(A^{\omega})$ .

Each state of an LMC corresponds to a unique stream distribution that records the probability of that state eventually emitting streams in a given Borel set. The following proposition is a special case of [9, Proposition 3.12].

Proposition 2.3.

Let $(X,\beta)$ be an LMC. There is a unique map $\left\llbracket{-}\right\rrbracket_{\beta}\colon X\to\text{\sf Prob}(A^{\omega})$ such that for any $x\in X$ and any $w\in A^{*}$ and $a\in A$ ,

\left\llbracket{x}\right\rrbracket_{\beta}(B_{aw})=\sum_{y\in X}\beta(x)(a,y)% \left\llbracket{y}\right\rrbracket_{\beta}(B_{w})

The map $\left\llbracket{-}\right\rrbracket_{\beta}$ above is the stream semantics of $(X,\beta)$ . Given states $x,y\in X$ , we say $x$ and $y$ are stream equivalent if $\left\llbracket{x}\right\rrbracket_{\beta}=\left\llbracket{y}\right\rrbracket_% {\beta}$ .

LMCs as coalgebras.

Universal coalgebra is by now a standard framework for studying state-based systems like LMCs [20]. The theory is sufficiently general for capturing systems where the states come with additional structure. Systems with structured state spaces are central to the main result of this paper, so we state the definitions below for more general categories than the category $\mathsf{Set}$ of sets and functions.

Definition 2.4.

Given an endofunctor on a category $F\colon\mathsf{C}\to\mathsf{C}$ , an $F$ -coalgebra is a pair $(X,c)$ consisting of an object $X$ of $\mathsf{C}$ and an arrow $c\colon X\to F(X)$ . A coalgebra homomorphism $h\colon(X,c^{X})\to(Y,c^{Y})$ is an arrow $h\colon X\to Y$ such that $c^{Y}\circ h=F(h)\circ c^{X}$ . We write $\mbox{\sf Coalg}_{\mathsf{C}}(F)$ for the category of $F$ -coalgebras and their homomorphisms.

The set-mapping $X\mapsto{\mathcal{D}}(X)$ is a functor, with action on functions given by

{\mathcal{D}}(f)(\theta)=\sum_{i=1}^{n}r_{i}\cdot f(x_{i})

where $f\colon X\to Y$ and $\theta=\sum_{i=1}^{n}r_{i}\cdot x_{i}$ . The set-mapping $X\mapsto A\times X$ is also a functor, with the action on functions being $f\mapsto\mathrm{id}_{A}\times f$ . By composition, ${\mathcal{D}}(A\times-)$ is an endofunctor on $\mathsf{Set}$ . The point is that LMCs are precisely ${\mathcal{D}}(A\times-)$ -coalgebras. Unravelling the definitions, a coalgebra homomorphism between LMCs $h\colon(X,\beta)\to(Y,\vartheta)$ is a function $h\colon X\to Y$ such that for any $x\in X$ , if $\beta(x)=\sum_{i=1}^{n}r_{i}\cdot(a_{i},x_{i})$ , then

\vartheta(h(x))=\sum_{i=1}^{n}r_{i}\cdot(a_{i},h(x_{i}))

Coalgebra homomorphisms are precisely the maps that preserve the branching-time behaviour of probabilistic systems.

A category $\mathsf{C}$ is concrete if there is a faithful functor $U\colon\mathsf{C}\to\mathsf{Set}$ . An object $X$ in a concrete category $\mathsf{C}$ is essentially a set $U(X)$ with additional structure, and arrows $X\to Y$ are functions that preserve that structure. We write $x\in X$ for $x\in U(X)$ . The category $\mathsf{Set}$ is of course concrete, as witnessed by the identity functor.

Definition 2.5.

Let $(X,c^{X})$ and $(Y,c^{Y})$ be $F$ -coalgebras where $F\colon\mathsf{C}\to\mathsf{C}$ and $\mathsf{C}$ is concrete, $x\in X$ and $y\in Y$ . We say $x$ and $y$ are behaviourally equivalent and write $x\sim y$ if there is a cospan $(X,c^{X})\stackrel{{\scriptstyle h}}{{\longrightarrow}}(Z,c^{Z})\stackrel{{% \scriptstyle k}}{{\longleftarrow}}(Y,c^{Y})$ in $\mbox{\sf Coalg}_{\mathsf{C}}(F)$ such that $h(x)=k(y)$ .

For LMCs, behavioural equivalence (which coincides with probabilistic bisimilarity) implies stream equivalence [21, Theorem 6.7].

Proposition 2.6.

Let $(X,\beta)$ and $(Y,\vartheta)$ be LMCs, $x\in X$ , $y\in Y$ . If $x\sim y$ , then $\left\llbracket{x}\right\rrbracket_{\beta}=\left\llbracket{y}\right\rrbracket_% {\vartheta}$ .

The converse fails: for LMCs, behavioural equivalence is strictly finer than stream equivalence (see, e.g., [21, Figure 8]). It follows that there is no LMC structure $(\text{\sf Prob}(A^{\omega}),c)$ such that $\left\llbracket{-}\right\rrbracket_{\beta}\colon(X,\beta)\to(\text{\sf Prob}(A% ^{\omega}),c)$ is always a coalgebra homomorphism.

3 Axiomatizing Stream Semantics

In this section, we recall Stark and Smolka’s specification language for probabilistic transition systems [29] and the axioms for trace equivalence proposed by Silva and Sokolova [25].

A Specification Language for LMCs

Fix an infinite set $V$ of variables. Consider the set of terms generated by the grammar below,

\displaystyle e,f::=v\mid ae\mid e\oplus_{r}f\mid\mu v\leavevmode\nobreak\ e

where $v\in V$ , $a\in A$ , and $r\in[0,1]$ . A variable $v$ is bound in a term $e$ if it appears within the scope of $\mu v\leavevmode\nobreak\ (-)$ , and guarded if it appears within the scope of some $a(-)$ . The set $\mathsf{PTerm}$ of productive process terms is the set of terms $e$ such that every variable $v$ appearing in $e$ is both guarded and bound. Given variables $v_{1},\dots,v_{n}$ , we write $\mathsf{PTerm}(v_{1},\dots,v_{n})$ for the set of guarded terms whose free variables are contained in $\{v_{1},\dots,v_{n}\}$ .

Intuitively, the operation $a(-)$ is prefixing by $a$ , and $a e$ denotes the process that makes an $a$ -labelled transition with probability $1$ into $e$ . The operations $\oplus_{r}$ are called convex sums, and $e\oplus_{r}f$ denotes the process whose outgoing transitions are the same as $e$ and $f$ , but with probabilities scaled by $r\in[0,1]$ and $1-r$ respectively. The operation $\mu v\leavevmode\nobreak\ (-)$ is recursion in $v$ , and $\mu v\leavevmode\nobreak\ g$ behaves exactly as $g[\mu v\leavevmode\nobreak\ g/v]$ does, where $g[\mu v\leavevmode\nobreak\ g/v]$ denotes the productive process term obtained by substituting every free occurrence of $v$ in $g$ with $\mu v\leavevmode\nobreak\ g$ . Recursion is the source of loops in the LMCs specified by productive process terms. The intuition behind each operation on productive process terms is formalized as follows.

Definition 3.1.

For any $e,f\in\mathsf{PTerm}$ , $a\in A$ , $v\in V$ , $g\in\mathsf{PTerm}(v)$ , and $r\in[0,1]$ , define

\displaystyle\tau(ae)=1\cdot(a,e)\quad\tau(e\oplus_{r}f)=r\leavevmode\nobreak% \ \tau(e)+(1-r)\leavevmode\nobreak\ \tau(f)\quad\tau(\mu v\leavevmode\nobreak% \ g)=\tau(g[\mu v\leavevmode\nobreak\ g/v])

Then $(\mathsf{PTerm},\tau)$ is the syntactic LMC.

Each probabilistic process term $e$ shares its stream semantics with a state in a finite LMC. In particular, let $\langle e\rangle$ be the set of probabilistic process terms $f$ such that $e\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{1}\mid r_{1}}$}}\cdots\mathrel{% \raisebox{-2.0pt}{$\xrightarrow{a_{n}\mid r_{n}}$}}f$ . Then $\langle e\rangle$ is finite and $\tau$ restricts to a transition structure $\tau_{\langle e\rangle}\colon\langle e\rangle\to{\mathcal{D}}(A\times\langle e\rangle)$ [21]. We also have $\left\llbracket{e}\right\rrbracket_{\tau}=\left\llbracket{e}\right\rrbracket_{% \tau_{\langle e\rangle}}$ , since $\left\llbracket{e}\right\rrbracket_{\tau}$ only depends on states reachable from $e$ .

The converse is also true. The following theorem, analogous to Kleene’s theorem for regular expressions [10], is a direct consequence of results presented in [29].

Theorem 3.2.

Let $(X,\beta)$ be a finite LMC and let $x\in X$ . There exists an $e\in\mathsf{PTerm}$ such that $e$ and $x$ are behaviourally equivalent.

As an immediate consequence of Theorems 3.2 and 2.6, we have that $\mathsf{PTerm}$ is a fully expressive specification language for states of finite LMCs.

Corollary 3.3.

Let $(X,\beta)$ be a finite LMC and let $x\in X$ . There exists an $e\in\mathsf{PTerm}$ such that $\left\llbracket{e}\right\rrbracket_{\tau}=\left\llbracket{x}\right\rrbracket_{\beta}$ .

From now on, we drop $\tau$ and simply write $\left\llbracket{e}\right\rrbracket$ instead of $\left\llbracket{e}\right\rrbracket_{\tau}$ , for $e\in\mathsf{PTerm}$ .

Example 3.4.

The state $x$ in the LMC (2.1) has the same stream semantics as the term $\mu v\leavevmode\nobreak\ (bv\oplus_{0.5}a(\mu u\leavevmode\nobreak\ (au\oplus% _{0.5}bv))))$ . However, it appears that there is a redundancy in the LMC (2.1). Both $x$ and $y$ emit $a$ and $b$ with the same probability, and each transitions to the other with the same probability. Thus, the stream semantics of both states $x$ and $y$ is the unique Borel probability distribution $\rho$ satisfying $\rho(B_{a_{1}\cdots a_{n}})=0.5^{n}$ for any $a_{1}\cdots a_{n}\in\{a,b\}^{*}$ , making $x$ and $y$ stream equivalent to the state $z$ below. This one-state LMC corresponds to the process term $\mu v\leavevmode\nobreak\ (av\oplus_{0.5}bv)$ .

It follows that $\left\llbracket{\mu v\leavevmode\nobreak\ (bv\oplus_{0.5}a(\mu u\leavevmode% \nobreak\ (au\oplus_{0.5}bv))))}\right\rrbracket=\left\llbracket{\mu v% \leavevmode\nobreak\ (av\oplus_{0.5}bv)}\right\rrbracket.$

Axioms for stream equivalence

As we have seen from Example 3.4, even very different looking productive process terms can be stream equivalent. To facilitate reasoning about equivalence, we give a set of inference rules for deducing algebraically that two productive process terms are stream equivalent.

Definition 3.5 (Provable equivalence).

Probabilistic process terms $e,f\in\mathsf{PTerm}$ are said to be provably equivalent, written $e\equiv f$ , if $e=f$ can be proven from axioms in Fig. 1. We write $[e]$ for the $\equiv$ -equivalence class of $e$ .

\displaystyle\begin{aligned} e&=e\oplus_{r}e\\ e_{1}\oplus_{r}e_{2}&=e_{2}\oplus_{1-r}e_{1}\\ (e_{1}\oplus_{r}e_{2})\oplus_{s}e_{3}&=e_{1}\oplus_{rs}(e_{2}\oplus_{\frac{s(1% -r)}{1-rs}}e_{3})\\ a(e_{1}\oplus_{r}e_{2})&=ae_{1}\oplus_{r}ae_{2}\end{aligned}\quad\begin{% gathered}\mu v\leavevmode\nobreak\ g=\mu u\leavevmode\nobreak\ g[u/v]\\ \mu v\leavevmode\nobreak\ g=g[\mu v\leavevmode\nobreak\ g/v]\\ f=\mu v\leavevmode\nobreak\ gf=g[f/v]\end{gathered}\quad\begin{gathered}ae_{1}% =ae_{2}e_{1}=e_{2}\\ e_{1}\oplus_{r}e_{2}=f_{1}\oplus_{r}f_{2}e_{1}=f_{1}\quad e_{2}=f_{2}\\ k[\vec{e}/\vec{v}]=k[\vec{f}/\vec{v}]e_{1}=f_{1}\ \dots\ e_{n}=f_{n}\end{gathered}

Figure 1: Axioms for probabilistic term equivalence. Above,

e,e_{i},f,f_{i}\in\mathsf{PTerm}

,

\vec{e}=(e_{1},\dots,e_{n})

,

\vec{f}=(f_{1},\dots,f_{n})

,

g\in\mathsf{PTerm}(v)

, and

k\in\mathsf{PTerm}(v_{1},\dots,v_{n})

. We assume that

u

is not bound in

g

in the first axiom of the second column. The term

k[\vec{e}/\vec{v}]

is obtained by simultaneously replacing

v_{i}

with

e_{i}

for each

i\leq n

. Note that the equivalence relation axioms are implicit. The difference with the axiomatization for bisimilarity is the distributivity axiom (lower-left).

The main goal of the paper is to prove that the axioms in Fig. 1 are sound and complete to reason about stream semantics of LMCs:

e\equiv f\quad\Longleftrightarrow\quad\llbracket e\rrbracket=\llbracket f% \rrbracket\qquad\qquad\qquad(\Longleftarrow):{\text{\footnotesize Completeness% }}\qquad(\Longrightarrow):{\text{\footnotesize Soundness}}

Soundness was established in [21, Theorem 6.9]. The main result in this paper is completeness, which verifies [21, Conjecture 1].

Theorem 3.6 (Completeness).

Let $e,f\in\mathsf{PTerm}$ . If $\left\llbracket{e}\right\rrbracket=\left\llbracket{f}\right\rrbracket$ , then $e\equiv f$ .

4 Blueprint for Proving Completeness

The main goal of the rest of the paper is to prove Theorem 3.6, completeness of our inference system. We begin with a high-level sketch of the proof to ease the flow into the upcoming technical sections. At the core of our argument will be the fact that the semantics of terms, as given by $\llbracket-\rrbracket$ , can be factorized:

(4.1)

The existence of this factorization is a consequence of soundness, which implies that $\left\llbracket{-}\right\rrbracket$ factors through the quotient $\mathsf{PTerm}/{\equiv}$ for a particular function $\partial^{\dagger}\colon\mathsf{PTerm}/{\equiv}\to\text{\sf Prob}(A^{\omega})$ . Once we have such factorization, we can reason as follows:

\displaystyle\left\llbracket{e}\right\rrbracket=\left\llbracket{f}\right% \rrbracket\quad\Longrightarrow\quad\partial^{\dagger}([e])=\partial^{\dagger}(% [f])\quad\stackrel{{\scriptstyle\star}}{{\Longrightarrow}}\quad[e]=[f]\quad% \Longrightarrow\quad e\equiv f

Now completeness follows if we can justify the $\star$ step, which amounts to injectivity of $\partial^{\dagger}$ . In other words, Theorem 3.6 follows if $\partial^{\dagger}$ is injective. And that is precisely what we are going to prove. Before we outline the completeness proof, we need a few notions from convex algebra.

Definition 4.1.

A convex algebra is an algebraic structure consisting of a set $X$ and a family of binary operations $\oplus_{p}\colon X\times X\to X$ (written infix) satisfying

\displaystyle x\oplus_{1}y=x\quad x\oplus_{r}x=x\quad x\oplus_{r}y=y\oplus_{1-% r}x\quad(x\oplus_{r}y)\oplus_{s}z=x\oplus_{rs}\Big{(}y\oplus_{\frac{s(1-r)}{1-% rs}}z\Big{)}

An affine map, or convex algebra homomorphism, between convex algebras $(X,\oplus^{X}_{p})$ and $(Y,\oplus^{Y}_{p})$ is a function $h\colon X\to Y$ that satisfies $h(x\oplus^{X}_{p}y)=h(x)\oplus^{Y}_{p}h(y)$ for each $p\in[0,1]$ . The category of convex algebras and affine maps is denoted $\mathsf{CA}$ .

A convex algebra $(X,\oplus^{X}_{p})$ is free and generated by a set $B\subseteq X$ if every map $f\colon B\to Y$ from $B$ to the carrier of a convex algebra $(Y,\oplus^{Y}_{p})$ extends to a unique affine map $f^{\#}\colon(X,\oplus^{X}_{p})\to(Y,\oplus^{Y}_{p})$ . The set $B$ is then the set of generators of the free algebra $(X,\oplus^{X}_{p})$ . If $B$ is a finite set, then the free algebra generated by $B$ is free finitely generated, ffg, for short. A convex algebra is finitely generated, fg, for short, if it is a homomorphic image of a free finitely generated one.

Note that we will often write $X$ instead of $(X,\oplus_{p})$ if the convex algebra structure is clear from the context.

Back to the intended completeness result as outlined above, we break the proof of injectivity of $\partial^{\dagger}$ into 3 steps, each of independent interest.

Step 1

We identify the category of convex algebras as the right base category to define the stream semantics of LMCs. More precisely, we define a functor $G$ on $\mathsf{CA}$ and show that the convex algebra of Borel probability distributions $\text{\sf Prob}(A^{\omega})$ carries a final $G$ -coalgebra structure $(\text{\sf Prob}(A^{\omega}),\zeta)$ . By turning any LMC $(X,\beta)$ into a $G$ -coalgebra $({\mathcal{D}}(X),\partial_{\beta})$ via a determinization construction (see Definition 5.11), we obtain the determinized stream semantics $(X,\beta)$ , $\llparenthesis{-}\rrparenthesis_{\beta}=\partial_{\beta}^{\dagger}\circ\eta% \colon X\to{\mathcal{D}}(X)\to\text{\sf Prob}(A^{\omega})$ via the final coalgebra homomorphism $\partial_{\beta}^{\dagger}\colon({\mathcal{D}}(X),\partial_{\beta})\to(\text{% \sf Prob}(A^{\omega}),\zeta)$ . We then relate this determinized stream semantics to the original stream semantics $\left\llbracket{-}\right\rrbracket$ defined in Proposition 2.3 using the syntactic LMC $(\mathsf{PTerm},\tau)$ as shown in the diagram (4.1).

Step 2

We provide a $G$ -coalgebra structure $(\mathsf{PTerm}/{\equiv},\partial)$ on the equivalence classes of terms modulo provable equivalence and show that every ffg $G$ -coalgebra $(X,\beta)$ (i.e., $X$ is ffg) has a unique coalgebra homomorphism into $(\mathsf{PTerm}/{\equiv},\partial)$ . This is related to solving certain systems of equations in $\mathsf{PTerm}/{\equiv}$ . We also show that $(\mathsf{PTerm}/{\equiv},\partial)$ is locally fg, in the following sense:

Definition 4.2.

A $G$ -coalgebra $(X,\gamma)$ is locally fg if for any $x\in X$ , there is a subcoalgebra $(U,\gamma_{U})$ of $(X,\gamma)$ such that $x\in U$ and $U$ is fg. A locally fg $G$ -coalgebra $(X,\gamma)$ is final if every locally fg $G$ -coalgebra admits a unique coalgebra homomorphism into $(X,\gamma)$ .

The significance of $(\mathsf{PTerm}/{\equiv},\partial)$ being locally fg is related to the lemma below.

Lemma 4.3.

Every homomorphic image of a locally fg $G$ -coalgebra is also locally fg.

Consider the surjective-injective factorization of the coalgebra homomorphism $\partial^{\dagger}$ below.

To show that $\partial^{\dagger}$ is injective, it suffices to show that the map $q$ has a left inverse, a coalgebra homomorphism $k\colon(J,\rho)\to(\mathsf{PTerm}/{\equiv},\partial)$ such that $k\circ q=\mathrm{id}$ , as then

\partial^{\dagger}([e])=\partial^{\dagger}([f])\Leftrightarrow\iota\circ q([e]% )=\iota\circ q([f])\Rightarrow q([e])=q([f])\Rightarrow k\circ q([e])=k\circ q% ([f])\Leftrightarrow[e]=[f].

One way to do this is to show that $(\mathsf{PTerm}/{\equiv},\partial)$ is the final locally fg $G$ -coalgebra. In such a case, by Lemma 4.3, $(J,\rho)$ is also locally fg, and therefore admits the desired (necessarily unique) coalgebra homomorphism $k$ . Indeed, by finality, since $k\circ q$ and $\mathrm{id}$ are both homomorphisms from $(\mathsf{PTerm}/{\equiv},\partial)$ to itself, they must be the same, i.e., $k\circ q=\mathrm{id}$ .

Step 3

Lastly, we will establish sufficient conditions guaranteeing that $(\mathsf{PTerm}/{\equiv},\partial)$ is the final locally fg $G$ -coalgebra. Our end goal will be to apply the following theorem, which can be obtained from a combination of [14, Corollary 5.9] and [27, Corollary 5.5].

Theorem 4.4.

Suppose that $F$ is a finitary proper endofunctor on $\mathsf{CA}$ that preserves surjective affine maps. Then an $F$ -coalgebra $(Y,\omega)$ is a final locally fg coalgebra if and only if (i) $(Y,\omega)$ is locally fg and (ii) for every ffg $F$ -coalgebra $({\mathcal{D}}(X),\partial_{\beta})$ , there is a unique coalgebra homomorphism $({\mathcal{D}}(X),\partial_{\beta})\to(Y,\omega)$ .

Theorem 4.4 uses the notion of a proper functor, which we will define in Definition 7.6 below.

After having completed Step 2, we will have already seen that $(\mathsf{PTerm}/{\equiv},\partial)$ is locally fg, and furthermore that every ffg $G$ -coalgebra admits a unique coalgebra homomorphism into $(\mathsf{PTerm}/{\equiv},\partial)$ . Thus, completing Step 3 hinges on showing that the functor $G$ is finitary, that it preserves surjective affine maps, and that $G$ is proper. Step 3 is the most technical of the three steps.
To summarize, here are our obligations stated in the three steps above:

1.

We must define $G:\mathsf{CA}\to\mathsf{CA}$ , endow $\text{\sf Prob}(A^{\omega})$ with a $G$ -coalgebra structure $\zeta$ , turning $\text{\sf Prob}(A^{\omega},\zeta)$ into a final $G$ -coalgebra.
2.

Given an LMC $(X,\beta)$ , we must explain how it is determinized to yield a $G$ -coalgebra $(\mathcal{D}(X),\partial_{\beta})$ , and how its stream semantics $\left\llbracket{-}\right\rrbracket$ is obtained from the final coalgebra homomorphism as $\left\llbracket{-}\right\rrbracket=\partial^{\dagger}_{\beta}\circ\eta$ . In other words, we must relate the stream semantics to the determinzed stream semantics $\llparenthesis{-}\rrparenthesis_{\beta}$ .
3.

We must define a coalgebra structure $\partial:\mathsf{PTerm}/{\equiv}\to G(\mathsf{PTerm}/{\equiv})$ and show that $(\mathsf{PTerm}/{\equiv},\partial)$ is locally fg and that free fg $G$ -coalgebras admit unique coalgebra homomorphisms into $(\mathsf{PTerm}/{\equiv},\partial)$ .
4.

We must show that $G$ is finitary, preserves surjective algebra homomorphisms, and is proper.

5 Step 1: Convex (Co)Algebras and the Functor $𝑮$

We begin executing each of the steps in Section 4. We first need some basic definitions on the category $\mathsf{CA}$ of convex algebras.

Convex algebras.

Recall that a convex algebra is an algebraic structure consisting of a set $X$ and a collection of convex sum operations $\oplus_{r}\colon X\times X\to X$ indexed by $r\in[0,1]$ satisfying the equations in Definition 4.1, and recall that we write $\mathsf{CA}$ for the category of convex algebras.

Example 5.1.

Prime examples of convex algebras are convex subsets of $\mathbb{R}^{n}$ , i.e., subsets $C\subseteq\mathbb{R}^{n}$ such that $\vec{p},\vec{q}\in C$ implies that $\vec{p}\oplus_{r}\vec{q}=r\vec{p}+(1-r)\vec{q}\in C$ for all $r\in[0,1]$ . Moreover, for any subset $U\subseteq\mathbb{R}^{n}$ , there is a smallest convex algebra containing $U$ , namely the convex hull $\operatorname{conv}(U)=\{r\vec{p}+(1-r)\vec{q}\mid\vec{p},\vec{q}\in U\text{ % and }r\in[0,1]\}$ .

We may use the following syntax as a generalized convex sum in an arbitrary convex algebra: given $r_{1},\dots,r_{n}\in(0,1)$ and $x_{1},\dots,x_{n}$ , define

\bigoplus_{i=1}^{n}r_{i}\cdot x_{i}=x_{n}\oplus_{r_{n}}\Big{(}\bigoplus_{i=1}^% {n-1}\frac{r_{i}}{1-r_{n}}\cdot x_{i}\Big{)}

(5.1)

It is important to note that, technically, the base case is $n=2$ . We can also use this notation if $r_{i}=0$ for $i\neq j$ and $r_{j}=1$ , but in that case we define $\bigoplus_{i=1}^{n}r_{i}\cdot x_{i}=x_{j}$ . Up to the convex algebra axioms, any two ways of reordering the summands of (5.1) produces equivalent terms. This justifies the slight abuse of notation $\bigoplus_{x\in S}r_{x}\cdot x$ , where $S$ is a set and $r_{(-)}\colon S\to[0,1]$ is a function such that $\sum_{x\in S}r_{x}=1$ and only finitely many of the $r_{x}$ are non-zero.

Free convex algebras.

$({\mathcal{D}}(X),\oplus_{p})$ is the free convex algebra generated by the set $X$ . Hence, for any convex algebra $(Y,\oplus^{Y}_{p})$ , and any function $f\colon X\to Y$ , there is a unique linear extension $f^{\#}\colon({\mathcal{D}}(X),\oplus_{p})\to(Y,\oplus^{Y}_{p})$ of $f$ such that $f^{\#}(1\cdot x)=f(x)$ . The universal property of free convex algebras gives rise to the adjunction $\cal F\dashv\cal U$ , where ${\cal F}(X)=({\mathcal{D}}(X),\oplus_{p})$ is the free functor that maps a set to the free convex algebra generated by it and a function $f\colon X\to Y$ to ${\mathcal{D}}(f)\colon{\mathcal{D}}(X)\to{\mathcal{D}}(Y)$ , and ${\cal U}$ is the forgetful functor from $\mathsf{CA}$ to $\mathsf{Set}$ that forgets the algebraic structure and is identity on homomorphisms.

The free functor $\cal F$ is a left adjoint to the forgetful functor, and clearly ${\mathcal{D}}={\cal U}\circ{\cal F}$ . It follows that $({\mathcal{D}},\eta,\mu)$ is a monad on $\mathsf{Set}$ with $\eta_{X}(x)=1\cdot x$ and $\mu_{X}=(\mathrm{id}_{{\mathcal{D}}(X)})^{\#}$ , and furthermore, $\mathsf{CA}$ is isomorphic to the category of Eilenberg-Moore algebras for ${\mathcal{D}}$ [31]. In particular, the free convex algebra generated by a set $X$ is the Eilenberg-Moore algebra $({\mathcal{D}}(X),\mu_{X})$ . We often omit writing the forgetful functor when no confusion arises, and (in accordance with our convention to drop the algebra structure when no confusion arises) also often just write ${\mathcal{D}}(X)$ for the free algebra ${\cal F}(X)$ .

Adding a fresh element $\bot$ to a convex algebra.

In order to define the endofunctor $G$ , we need the following construction on convex algebras. Given a convex algebra $X$ , define $X_{\bot}=\{\bot\}\cup\{r\cdot x\mid r\in(0,1],x\in X\}$ . The set $X_{\bot}$ obtains a convex algebra structure with respect to the convex sum operation defined

	$\displaystyle\bot\oplus_{q}\bot=\bot\qquad r\cdot x\oplus_{q}\bot=(qr)\cdot x% \qquad\bot\oplus_{q}s\cdot y=((1-q)s)\cdot y$
	$\displaystyle r\cdot x\oplus_{q}s\cdot y=(qr+(1-q)s)\cdot(x\oplus_{\frac{qr}{% qr+(1-q)s}}y)$

Lemma 5.2.

Let $X$ be a convex algebra. As defined above, $(X_{\bot},\oplus)$ is a convex algebra. Moreover, given $r\cdot x$ and $s\cdot y$ in $X_{\bot}$ , $r\cdot x=s\cdot y$ if and only if $r=s$ and $x=y$ .

$\blacktriangleright$ Remark 5.3.

We introduce some notation going forwards. We often use the notation $0\cdot x$ for $\bot$ , even implicitly, despite that $0\cdot x=0\cdot y$ for all $x,y\in X$ .

The construction $(-)_{\bot}\colon\mathsf{CA}\to\mathsf{CA}$ is a functor whose action on convex algebra homomorphisms is given by $h_{\bot}(r\cdot x)=r\cdot h(x)$ for any convex algebra homomorphism $h\colon(X,\oplus_{p})\to(Y,\oplus_{p})$ and any $x\in X$ . The homomorphism $h_{\bot}$ additionally satisfies $h_{\bot}(\bot)=\bot$ . Freely adjoining $\bot$ is analogous to going from probability distributions to sub-probability distributions (maps $\theta\colon X\to[0,1]$ such that $\sum_{x\in X}\theta(x)\leq 1$ ). The following lemma makes this precise.

Lemma 5.4.

Let ${\mathcal{D}}_{\bot}$ be the finitely supported sub-probability distribution functor, and let $\text{\sf Prob}_{\bot}(A^{\omega})$ be the set of Borel sub-probability measures on $A^{\omega}$ . Then as convex algebras, ${\mathcal{D}}(X)_{\bot}\cong{\mathcal{D}}_{\bot}(X)$ and $\text{\sf Prob}(A^{\omega})_{\bot}\cong\text{\sf Prob}_{\bot}(A^{\omega})$ .

The functor $G:\mathsf{CA}\to\mathsf{CA}$

We are now ready to introduce the functor on $\mathsf{CA}$ needed to move from $\mathsf{Set}$ to $\mathsf{CA}$ . There are different ways to define such a functor, e.g. Silva and Sokolova [25] use another functor for the axiomatization of finite trace semantics. The choice of the “right” functor so that our intended results go through, i.e., the choice of this particular functor $G$ , is one of the main contributions of this paper.

Given a convex algebra $X$ and a convex algebra homomorphism $h\colon X\to Y$ , let

G(X)=\Big{\{}f:A\to X_{\bot}\,\mid\ \sum_{a\in A}r_{a}^{f}=1\Big{\}}\qquad G(h% )(f)(a)=r_{a}^{f}\cdot h(x_{a}^{f})

(5.2)

where $f(a)=r_{a}^{f}\cdot x_{a}^{f}$ for each $f\in G(X)$ and $a\in A$ . Equivalently, $G(h)(f)=h_{\bot}\circ f$ . Note that in the definition of $G(X)$ above, the sum is the usual sum of real numbers, and that we define $r_{a}^{f}=0$ and leave $x_{a}^{f}$ undefined when $f(a)=\bot$ .

Proposition 5.5.

As it is defined in (5.2), $G$ is an endofunctor on $\mathsf{CA}$ .

We use the following terminology to refer to the defining property of $G$ : If $f:A\to X_{\bot}$ has the property that $\sum_{a}r_{a}^{f}=1$ , as mentioned in (5.2), we say that $f$ satisfies the mass-splitting property, or that $f$ is mass splitting.¹¹1The mass-splitting property was inspired by a condition in Goy and Rot’s paper [6, Proposition 4.5].

In particular, a function $f\colon A\to{\mathcal{D}}_{\bot}(X)$ is mass splitting, i.e., $f\in G({\mathcal{D}}(X))$ , if and only if the total mass $\sum_{a\in A}\sum_{x\in X}f(a)(x)$ is equal to $1$ . Given such a function, one can reverse-engineer a unique probability distribution $\theta\in{\mathcal{D}}(A\times X)$ such that $f$ computes the marginal $f(a)=\theta(\{a\}\times X)$ for each $a\in A$ . Thus, a $G$ -coalgebra of the form $({\mathcal{D}}(X),\gamma)$ represents the same data as an LMC $(X,\beta)$ by reverse-engineering $\beta(x)$ from $\gamma(1\cdot x)$ for each $x\in X$ . We think of $G$ -coalgebras as the deterministic counterpart of LMCs. Their exact relationship will be made precise at the end of this section.

$\blacktriangleright$ Remark 5.6.

Note that as a set, $X_{\bot}\cong 1+(0,1]\times X$ , and so the description of $G(X)$ above can also be taken as a definition of a functor $H\colon\mathsf{Set}\to\mathsf{Set}$ . Indeed, $G$ is a lifting of $H$ to $\mathsf{CA}$ . However, the convex algebra structure on $X_{\bot}$ is not the convex algebra structure on $1+(0,1]\times X$ obtained from (co)products in $\mathsf{CA}$ . The convex algebra structure is instead hand-tailored to match the structure of sub-probability distributions.

In a given $G$ -coalgebra $(X,\gamma)$ , we write $\mbox{\sf mass}_{\gamma}(a,x)$ for $r_{a}^{\gamma(x)}$ , and whenever $r_{a}^{\gamma(x)}>0$ , we write $\mbox{\sf next}_{\gamma}(a,x)$ for $x_{a}^{\gamma(x)}$ . Then whenever $\gamma(x)(a)=\bot$ , $\mbox{\sf mass}_{\gamma}(a,x)=0$ while $\mbox{\sf next}_{\gamma}(a,x)$ is undefined; and when $\mbox{\sf mass}_{\gamma}(a,x)>0$ ,

\gamma(x)(a)=\mbox{\sf mass}_{\gamma}(a,x)\cdot\mbox{\sf next}_{\gamma}(a,x).

(5.3)

where the $\cdot$ symbol here is from $X_{\bot}$ . Note that we often drop $\gamma$ and write simply mass and next. In this notation, the mass-splitting property says that for all $x\in X$ , we have $\sum_{a\in A}\mbox{\sf mass}(a,x)=1$ .

Given $G$ -coalgebras $(X,\gamma)$ and $(Y,\omega)$ , unravelling the definitions of mass and next reveals that a function $h:X\to Y$ is a coalgebra homomorphism if and only if

\mbox{\sf mass}(a,x)\cdot h(\mbox{\sf next}(a,x))=\mbox{\sf mass}(a,h(x))\cdot% \mbox{\sf next}(a,h(x))

(5.4)

for any $a\in A$ and $x\in X$ . In other words, for all $x\in X$ and $a\in A$ , $\mbox{\sf mass}(a,x)=\mbox{\sf mass}(a,h(x))$ , and if this is greater than $0$ , then $h(\mbox{\sf next}(a,x))=\mbox{\sf next}(a,h(x))$ as well.

A final $𝑮$ -coalgebra.

We are now in the position to show that $\text{\sf Prob}(A^{\omega})$ is the carrier of a final $G$ -coalgebra. First, observe that, like ${\mathcal{D}}(X)$ , $\text{\sf Prob}(A^{\omega})$ is a convex algebra with the canonical convex sums, $\rho\oplus_{r}\theta=r\rho+(1-r)\theta$ . In the proof of Theorem 5.13, we use the ${\mathcal{D}}$ -algebra in the more general, Eilenberg-Moore, form $(\text{\sf Prob}(A^{\omega}),\Sigma)$ , where

\Sigma(\sum\limits_{i=1}^{n}r_{i}\cdot\rho_{i})(B)=\sum\limits_{i=1}^{n}r_{i}% \rho_{i}(B)

(5.5)

Definition 5.7.

The $G$ -coalgebra structure $(\text{\sf Prob}(A^{\omega}),\zeta)$ is given by, for $\rho\in\text{\sf Prob}(A^{\omega})$ ,

\zeta(\rho)(a)=\left\{\begin{array}[]{ll}\bot&\mbox{if $\rho(B_{a})=0$}\\ \rho(B_{a})\cdot\big{(}B\mapsto\rho(aB)/\rho(B_{a})\big{)}&\mbox{if $\rho(B_{a% })>0$}\end{array}\right.

(5.6)

where for Borel $B$ , $aB=\{(a,a_{1},\dots)\mid(a_{1},\dots)\in B\}$ is the Borel set obtained by prefixing.

It is easy to check that $\zeta$ is a convex algebra homomorphism and that $\zeta(\rho)$ satisfies the mass-splitting property for each $\rho\in\text{\sf Prob}(A^{\omega})$ .

$\blacktriangleright$ Remark 5.8.

It is important to note that $\mbox{\sf next}_{\zeta}(a,-)\colon\text{\sf Prob}(A^{\omega})\to\text{\sf Prob% }(A^{\omega})$ is not (in general) a convex algebra homomorphism.

Theorem 5.9.

The $G$ -coalgebra $(\text{\sf Prob}(A^{\omega}),\zeta)$ is final. That is, for any $G$ -coalgebra $(X,\gamma)$ , there is a unique coalgebra homomorphism $\gamma^{{\dagger}}\colon(X,\gamma)\to(\text{\sf Prob}(A^{\omega}),\zeta)$ .

Here is a hint of a hint. We define $\gamma^{{\dagger}}(x)(B_{w})\in[0,1]$ by recursion on the length of $w$ :

	$\displaystyle\gamma^{{\dagger}}(x)(B_{\varepsilon})$	$\displaystyle=1$		(5.7)
	$\displaystyle\gamma^{\dagger}(x)(B_{aw})$	$\displaystyle=\begin{cases}0&\text{if $\gamma(x)(a)=\bot$}\\ \mbox{\sf mass}(a,x)\cdot\gamma^{\dagger}(\mbox{\sf next}(a,x))(B_{w})&\text{% if $\gamma(x)(a)\neq\bot$}\end{cases}$		(5.7)

One needs to show that this specifies each function $\gamma^{{\dagger}}$ as a finitely additive function on the generators of the Borel algebra, that the resulting function $\gamma^{\dagger}$ is a convex algebra morphism as well as a $G$ -coalgebra morphism, and finally that it is the unique such map.

$\blacktriangleright$ Remark 5.10.

It is also true that (forgetting the convex algebra structure) $\text{\sf Prob}(A^{\omega})$ is the final coalgebra of the functor $H:\mathsf{Set}\to\mathsf{Set}$ mentioned in Remark 5.6. This provides a way to define the stream semantics of LMCs using finality (Proposition 2.3), i.e., without the convex algebra structure. However, other ingredients in our completeness proof do require convex algebras.

Determinization: Connecting LMCs and $𝑮$ -coalgebras

Earlier in this section, we mentioned that one can think of $G$ -coalgebras as deterministic counterparts to LMCs. We now make the relationship between LMCs and $G$ -coalgebras precise. Using the universal property of free convex algebras and the correspondence between finitely supported probability distributions $\theta\in{\mathcal{D}}(A\times-)$ and functions $f\colon A\to{\mathcal{D}}_{\bot}(-)$ satisfying the mass-splitting property, we can construct a determinization functor $\Delta\colon\mbox{\sf Coalg}_{\mathsf{Set}}({\mathcal{D}}(A\times-))\to\mbox{% \sf Coalg}_{\mathsf{CA}}(G)$ as follows.

First, we define the natural transformation $\lambda_{Y}:{\mathcal{D}}(A\times Y)\to G({\mathcal{D}}(Y))$ by

\lambda_{Y}(\theta)(a)=\begin{cases}\bot&\mbox{if $s_{a}=0$}\\ s_{a}\cdot(\frac{1}{s_{a}}\theta(a,-))&\mbox{otherwise}\end{cases}

(5.8)

for each set $Y$ , $\theta\in{\mathcal{D}}(A\times Y)$ , and $a\in A$ , with $s_{a}=\sum_{y\in Y}\theta(a,y)$ . After making the identification ${\mathcal{D}}(X)_{\bot}={\mathcal{D}}_{\bot}(X)$ , this amounts to $\lambda_{Y}(\theta)(a)(x)=\theta(a,x)$ . A routine check verifies that $\lambda_{Y}$ is natural in $Y$ and that for any $\theta\in{\mathcal{D}}(A\times Y)$ , $\lambda_{Y}(\theta)$ satisfies the mass-splitting property.

Having constructed $\lambda$ , we can now define the determinization $\Delta(Y,\beta)$ of the LMC $(Y,\beta)$ to be the linear extension of the composition of $\lambda_{Y}$ after $\beta$ .

Definition 5.11.

The determinization functor $\Delta\colon\mbox{\sf Coalg}_{\mathsf{Set}}({\mathcal{D}}(A\times-))\to\mbox{% \sf Coalg}_{\mathsf{CA}}(G)$ is the functor given by $\Delta(Y,\beta)=(({\mathcal{D}}(Y),\mu_{Y}),\partial_{\beta})$ with $\partial_{\beta}=(\lambda_{Y}\circ\beta)^{\#}$ for any LMC $(Y,\beta)$ , and $\Delta(h)={\mathcal{D}}(h)$ for any coalgebra homomorphism $h$ between LMCs.

Moreover, we can show that $\lambda$ is a natural isomorphism, by providing an inverse transformation $\chi_{Y}:G({\mathcal{D}}(Y))\to{\mathcal{D}}(A\times Y)$ . For $h\in G({\mathcal{D}}(Y))$ with $h(a)=r_{a}\cdot h_{a}$ , define

\chi_{Y}(h)(a,y)=\begin{cases}0&h(a)=\bot\\ r_{a}h_{a}(y)&\text{otherwise}\end{cases}

(5.9)

Proposition 5.12.

The natural transformations $\lambda$ and $\chi$ are inverse to each other. Moreover, given a $G$ -coalgebra $(({\mathcal{D}}(Y),\mu_{Y}),\gamma)$ , let $\beta:Y\to{\mathcal{D}}(A\times Y)$ be given by $\beta=\chi_{Y}\circ\gamma\circ\eta_{Y}$ . Then $(({\mathcal{D}}(Y),\mu_{Y}),\gamma)=\Delta(Y,\beta)$ . As a result, a $G$ -coalgebra is ffg iff it is a determinized finite LMC.

By Theorem 5.9, $(\text{\sf Prob}(A^{\omega}),\zeta)$ is a final $G$ -coalgebra, so from any LMC $(Y,\beta)$ , we may determinize to get a $G$ -coalgebra $\Delta(Y,\beta)$ and then use finality to obtain a unique coalgebra homomorphism $\partial_{\beta}^{\dagger}\colon\Delta(Y,\beta)\to((\text{\sf Prob}(A^{\omega}% ),\Sigma),\zeta)$ . This yields a determinized stream semantics map $\llparenthesis{-}\rrparenthesis_{\beta}:Y\to\text{\sf Prob}(A^{\omega})$ by composition, i.e., $\llparenthesis{\,y\,}\rrparenthesis_{\beta}=\partial_{\beta}^{\dagger}(1\cdot y)$ . Fulfilling its intended purpose, determinized stream semantics does indeed coincide with stream semantics as we previously defined it.

Theorem 5.13.

For every LMC $(X,\beta)$ , $\llparenthesis{-}\rrparenthesis_{\beta}=\left\llbracket{-}\right\rrbracket_{% \beta}\,.$

Proof.

Let $\alpha:{\mathcal{D}}(A\times\text{\sf Prob}(A^{\omega}))\to\text{\sf Prob}(A^{% \omega})$ be given by $\alpha(\theta)(B_{\varepsilon})=1$ , and for all $a\in A$ , $w\in A^{*}$ ,

\alpha(\theta)(B_{aw})=\sum\limits_{\rho\in\text{\sf Prob}(A^{\omega})}\theta(% a,\rho)\,\rho(B_{w})

(5.10)

For a fixed $\theta\in{\mathcal{D}}(A\times\text{\sf Prob}(A^{\omega}))$ , let us use the notation $s_{a}$ for $\sum_{\rho\in\text{\sf Prob}(A^{\omega})}\theta(a,\rho)$ . Note that taking $w$ in (5.10) to be the empty word $\varepsilon$ gives $s_{a}=\alpha(\theta)(B_{a})$ .

Fix $(X,\beta)$ . Let us first check that a map $f:X\to\text{\sf Prob}(A^{\omega})$ satisfies the equation mentioned in Proposition 2.3 if and only if $f=\alpha\circ{\mathcal{D}}(A\times f)\circ\beta$ . That is, $f(x)(B_{aw})=\sum_{y\in X}(\beta(x)(a,y))(f(y)(B_{w}))$ for all $a\in A$ and $w\in A^{*}$ if and only if $f=\alpha\circ{\mathcal{D}}(A\times f)\circ\beta$ . This follows from:

	$\displaystyle(\alpha\circ{\mathcal{D}}(A\times f)\circ\beta)(x)(B_{aw})$	$\displaystyle=\sum\limits_{\rho\in\text{\sf Prob}(A^{\omega})}({\mathcal{D}}(A% \times f)(\beta(x))(a,\rho))\rho(B_{w})$
		$\displaystyle=\sum\limits_{\rho\in\text{\sf Prob}(A^{\omega})}\left(\sum% \limits_{y:f(y)=\rho}\beta(x)(a,y)\right)\rho(B_{w})$
		$\displaystyle=\sum\limits_{y\in X}(\beta(x)(a,y))(f(y)(B_{w}))$

where the first equality is by the definition of $\alpha$ , the second equality is the definition of ${\mathcal{D}}(A\times f)$ , and the third only rearranges the sum.

In the notation of Proposition 2.3, the map $\left\llbracket{-}\right\rrbracket=\left\llbracket{-}\right\rrbracket_{\beta}$ is the unique map so that $\left\llbracket{-}\right\rrbracket=\alpha\circ\mathcal{D}(A\times\left% \llbracket{-}\right\rrbracket)\circ\beta$ . So we shall show that the $\llparenthesis{-}\rrparenthesis$ has this same property. We thus show the commutativity of the outer diagram below (with arrows in blue):

The top square commutes by definition of $\llparenthesis{-}\rrparenthesis$ , the left part commutes as $\partial_{\beta}\circ\eta=\lambda\circ\beta$ by definition of $\partial_{\beta}$ , the middle square commutes because $\partial_{\beta}^{\dagger}$ is a coalgebra homomorphism, and the part on the bottom commutes by naturality of $\lambda$ . The commutativity of the remaining two parts is shown below.

We first prove that $\zeta\circ\alpha=G(\Sigma)\circ\lambda$ , giving commutativity of the part on the right. For $\theta\in{\mathcal{D}}(A\times\text{\sf Prob}(A^{\omega}))$ , $a\in A$ , and $w\in A^{*}$ , we have, on the one hand:

	$\displaystyle\alpha(\theta)(B_{aw})$	$\displaystyle=\sum_{\rho\in\text{\sf Prob}(A^{\omega})}\theta(a,\rho)\rho(B_{w})$
	$\displaystyle\zeta(\alpha(\theta))(a)$	$\displaystyle=\left\{\begin{array}[]{ll}\bot&\mbox{if $s_{a}=0$}\\ s_{a}\cdot(B_{w}\mapsto\sum_{\rho\in\text{\sf Prob}(A^{\omega})}\frac{\theta(a% ,\rho)}{s_{a}}\rho(B_{w}))&\mbox{if $s_{a}\neq 0$}\end{array}\right.$		(5.13)

We have used definitions of $\alpha$ from (5.10) and $\zeta$ from (5.6), that $aB_{w}=B_{aw}$ and that $\alpha(\theta)(B_{a})=s_{a}$ . On the other hand, we use the definitions of $\lambda$ from (5.8) and $\Sigma$ from (5.5):

	$\displaystyle\lambda_{\text{\sf Prob}(A^{\omega})}(\theta)(a)$	$\displaystyle=\begin{cases}\bot&\mbox{if $s_{a}=0$}\\ s_{a}\cdot(\rho\mapsto\frac{\theta(a,\rho)}{s_{a}})&\mbox{if $s_{a}\neq 0$}% \end{cases}$
	$\displaystyle G(\Sigma)(\lambda_{\text{\sf Prob}(A^{\omega})}(\theta))(a)$	$\displaystyle=\begin{cases}\bot&\mbox{if $s_{a}=0$}\\ s_{a}\cdot(B_{w}\mapsto\sum_{\rho\in\text{\sf Prob}(A^{\omega})}\frac{\theta(a% ,\rho)}{s_{a}}\rho(B_{w}))&\mbox{if $s_{a}\neq 0$}\end{cases}$		(5.14)

Equations (5) and (5) now give $\zeta\circ\alpha=G(\Sigma)\circ\lambda$ .

We turn to the commutativity of the remaining square. First, affineness of the map $\partial_{\beta}^{\dagger}:{\mathcal{D}}X\to\text{\sf Prob}(A^{\omega})$ yields $\partial_{\beta}^{\dagger}\circ\mu_{X}=\Sigma\circ{\mathcal{D}}(\partial_{% \beta}^{\dagger})$ . We precompose with ${\mathcal{D}}(\eta_{X})$ , and use the monad law $\mu_{X}\circ{\mathcal{D}}(\eta_{X})=\mathrm{id}_{{\mathcal{D}}X}$ along with the definition of $\llparenthesis{-}\rrparenthesis$ . Thus $\partial_{\beta}^{\dagger}=\Sigma\circ{\mathcal{D}}(\llparenthesis{-}\rrparenthesis)$ . Now apply $G$ to see the desired commutativity. $\hfill\blacktriangleleft$

Returning to our blueprint for completeness in Section 4, Theorem 5.13 shows that $\left\llbracket{-}\right\rrbracket$ arises from the final coalgebra map of $(\mathsf{PTerm},\tau)$ .

6 Step 2: $\mathsf{PTerm}/{\equiv}$ as a $𝑮$ -coalgebra

The set $\mathsf{PTerm}/{\equiv}$ of provable equivalence classes of productive process terms inherits a canonical convex algebra structure from $\mathsf{PTerm}$ , given by $[e]\oplus_{r}[f]=[e\oplus_{r}f]$ . These operations are well-defined because Fig. 1 includes the necessary axiom and they are indeed convex operations as Fig. 1 includes the convex algebra axioms. In this section, we show that $\mathsf{PTerm}/{\equiv}$ also carries a canonical $G$ -coalgebra structure $(\mathsf{PTerm}/{\equiv},\partial)$ . We then focus on two goals: The first goal is to show that the stream semantics of a productive process term $e$ is equal to the stream distribution $\partial^{\dagger}([e])$ obtained from the finality of $(\text{\sf Prob}(A^{\omega}),\zeta)$ . The second goal of this section is to show that $(\mathsf{PTerm}/{\equiv},\partial)$ is locally fg and that every ffg $G$ -coalgebra admits a unique coalgebra homomorphism into $(\mathsf{PTerm}/{\equiv},\partial)$ .

Defining $\partial$ .

Let $\tau(e)=\sum_{i=1}^{n}r_{i}\cdot(a_{i},e_{i})$ and write $s_{a}=\sum_{a_{i}=a}r_{i}$ . We define the map $\partial\colon\mathsf{PTerm}/{\equiv}\to G(\mathsf{PTerm}/{\equiv})$ using the formulas

\mbox{\sf mass}_{\partial}(a,[e])=\sum_{a_{i}=a}r_{i}\qquad\mbox{\sf next}_{% \partial}(a,[e])=\Big{[}\bigoplus_{i=1}^{n}(r_{i}/s_{a})\cdot e_{i}\Big{]}

(6.1)

for any $\equiv$ -equivalence class $[e]\in\mathsf{PTerm}/{\equiv}$ and $a\in A$ . It can be shown by induction on derivations that (6.1) describes a well-defined map, i.e., $e\equiv f$ implies the right-hand sides of the equations in (6.1) agree.

The following characterization of $(\mathsf{PTerm}/{\equiv},\partial)$ illustrates that this is a natural choice of $G$ -coalgebra structure on $\mathsf{PTerm}/{\equiv}$ .

Lemma 6.1.

Given $e_{1},e_{2}\in\mathsf{PTerm}$ , let

\tau(e_{1})=\sum_{i=1}^{n}r_{i}\cdot(a_{i},f_{i})\qquad\tau(e_{2})=\sum_{i=1}^% {n}s_{i}\cdot(a_{i},f_{i})

If $e_{1}\equiv e_{2}$ , then for any $a\in A$ ,

r_{a}=s_{a}\qquad\text{ and }\qquad\bigoplus_{i=1}^{n}(r_{i}/r_{a})\cdot f_{i}% \equiv\bigoplus_{i=1}^{n}(s_{i}/s_{a})\cdot f_{i}

(6.2)

where $r_{a}=\sum_{a_{i}=a}r_{i}$ and $s_{a}=\sum_{a_{i}=a}s_{i}$ .

The proof of Lemma 6.1 is a rather long induction on the proof of $e\equiv f$ . As an immediate consequence of this lemma, we obtain the following.

Lemma 6.2.

Let $({\mathcal{D}}(\mathsf{PTerm}),\partial_{\tau})=\Delta(\mathsf{PTerm},\tau)$ and $h_{\Sigma}=([-])^{\#}$ be the linear extension of the quotient-by- $\equiv$ map. Then the following diagram commutes.

(6.3)

In particular, $\partial$ is a convex algebra homomorphism, and $(\mathsf{PTerm}/{\equiv},\partial)$ is a homomorphic image of the determinized syntactic LMC.

Theorem 6.3.

For any $e\in\mathsf{PTerm}$ , $\left\llbracket{e}\right\rrbracket=\partial^{\dagger}([e])$ .

Proof.

By Theorem 5.9 and Theorem 5.13, $\left\llbracket{e}\right\rrbracket=\partial_{\tau}^{\dagger}(1\cdot e)=% \partial^{\dagger}\circ h_{\Sigma}(1\cdot e)=\partial^{\dagger}([e])$ . $\hfill\blacktriangleleft$

Theorem 6.4.

The $G$ -coalgebra $(\mathsf{PTerm}/{\equiv},\partial)$ is locally fg.

Proof.

It follows from results due to Stark and Smolka [29] that the syntactic LMC $(\mathsf{PTerm},\tau)$ is locally finite, in the sense that for any $e\in\mathsf{PTerm}$ , there is a finite subcoalgebra $(U,\tau_{U})$ of $(\mathsf{PTerm},\tau)$ containing $e$ . So, let $[e]\in\mathsf{PTerm}/{\equiv}$ and find a finite subcoalgebra $(U,\tau_{U})$ of $(\mathsf{PTerm},\tau)$ containing $e$ . Then $\Delta(U,\tau_{U})$ is a free fg subcoalgebra of $\Delta(\mathsf{PTerm},\tau)=({\mathcal{D}}(\mathsf{PTerm}),\partial_{\tau})$ containing $1\cdot e$ . Taking the image of $\Delta(U,\tau_{U})$ under $h_{\Sigma}$ , we obtain a finite subcoalgebra $(V,\partial_{V})=h_{\Sigma}(\Delta(U,\tau_{U}))$ of $(\mathsf{PTerm}/{\equiv},\partial)$ containing $[e]=h_{\Sigma}(1\cdot e)$ , as a quotient of a free fg $G$ -coalgebra. Thus, $[e]$ is contained in a fg subcoalgebra. $\hfill\blacktriangleleft$

Systems of equations from $𝑮$ -coalgebras and their unique solutions

The next goal is to show that every ffg $G$ -coalgebra admits a unique coalgebra homomorphism into $(\mathsf{PTerm}/{\equiv},\partial)$ . As we remarked after Definition 5.11, every ffg $G$ -coalgebra is of the form $\Delta(X,\beta)$ for some finite LMC $(X,\beta)$ . So, it suffices to show that every determinized finite LMC admits a unique coalgebra homomorphism into $\mathsf{PTerm}/{\equiv}$ . As we will see, each coalgebra homomorphism $\Delta(X,\beta)\to(\mathsf{PTerm}/{\equiv},\partial)$ corresponds to a solution to a particular system of equations.

Definition 6.5.

The guarded system of equations corresponding to the finite LMC $(X,\beta)$ is the set of formal equations

\mathcal{S}(X,\beta)=\Big{\{}x=\leavevmode\nobreak\ \bigoplus_{\mathclap{(a,y)% \in A\times X}}\leavevmode\nobreak\ \beta(x)(a,y)\cdot ay\leavevmode\nobreak\ % \Big{|}\leavevmode\nobreak\ x\in X\Big{\}}

(6.4)

A solution to the guarded system of equations (6.4) is a map

\varphi\colon X\to\mathsf{PTerm}\qquad\text{such that}\qquad(\forall x\in X)% \leavevmode\nobreak\ \varphi(x)\equiv\leavevmode\nobreak\ \bigoplus_{\mathclap% {(a,y)\in A\times X}}\leavevmode\nobreak\ \beta(x)(a,y)\cdot a\varphi(y)

Two solutions $\varphi,\psi$ are equivalent, written $\varphi\equiv\psi$ , if $\varphi(x)\equiv\psi(x)$ for all $x\in X$ .

The following theorem was a key component of Stark and Smolka’s completeness proof for bisimilarity.

Theorem 6.6 (Stark-Smolka [29]).

Every guarded finite system of equations has a unique solution up to $\equiv$ without the use of the distributivity axiom $a(e\oplus_{r}f)=ae\oplus_{r}af$ .

An immediate consequence of the above theorem is the existence and uniqueness of solutions for systems of equations that arise from LMCs.

Corollary 6.7.

Let $(X,\beta)$ be a finite LMC. Then $\mathcal{S}(X,\beta)$ has a unique solution up to $\equiv$ .

Using the distributivity axiom, we can transform each equation in (6.4) into an equivalent system of equations of the form

x=\bigoplus_{a\in A}\mbox{\sf mass}(a,x)\cdot a\leavevmode\nobreak\ \mbox{\sf next% }(a,x)

where mass and next are derived from $\partial_{\beta}$ . This tells us that a map $\varphi\colon X\to\mathsf{PTerm}$ is a solution to $\mathcal{S}(X,\beta)$ if and only if for all $x\in X$ ,

\varphi(x)\equiv\bigoplus_{a\in A}\mbox{\sf mass}(a,x)\cdot a\leavevmode% \nobreak\ \varphi(\mbox{\sf next}(a,x))

Solving systems of equations of this form is equivalent to finding $G$ -coalgebra homomorphisms into $(\mathsf{PTerm}/{\equiv},\partial)$ .

Lemma 6.8.

Let $(X,\beta)$ be a finite LMC, and let $\varphi\colon X\to\mathsf{PTerm}$ . Define $s_{\beta}\colon{\mathcal{D}}(X)\to\mathsf{PTerm}/{\equiv}$ to be the linear extension of the composition $[-]\circ\varphi\colon X\to\mathsf{PTerm}/{\equiv}$ . Then $\varphi$ is a solution to $\mathcal{S}(X,\beta)$ if and only if $s\colon\Delta(X,\beta)\to(\mathsf{PTerm}/{\equiv},\partial)$ is a coalgebra homomorphism.

We immediately obtain the following theorem.

Theorem 6.9.

Let $(X,\beta)$ be a finite LMC. There is a unique $G$ -coalgebra homomorphism $s_{\beta}\colon\Delta(X,\beta)\to(\mathsf{PTerm}/{\equiv},\partial)$ .

Hence, recalling that every ffg coalgebra arises via determinisation (see Proposition 5.12) yields that we have a unique homomorphism from any ffg coalgebra to $(\mathsf{PTerm}/{\equiv},\partial)$ .

7 Step 3: Properness of $𝑮$

In this section, we finish the outline of completeness that we stated in Section 4 by establishing that $G$ is finitary, preserves surjective affine maps, and is proper. By Theorems 4.4, 6.4, and 6.9, this allows us to conclude that $(\mathsf{PTerm}/{\equiv},\partial)$ is the final locally fg $G$ -coalgebra.

Lemma 7.1.

$G$ preserves pullbacks, and hence monomorphisms.

Let us mention that monomorphisms in $\mathsf{CA}$ are exactly those affine maps which are injective as set functions. This follows from the fact that $U\colon\mathsf{CA}\to\mathsf{Set}$ is a right adjoint and thus preserves all limits, in particular all pullbacks. Recall that in any category monos are characterized as special pullbacks as in the square below. In particular, let $f:X\to Y$ be a monomorphism in $\mathsf{CA}$ . Then the square below is a pullback (and conversely) in $\mathsf{CA}$ .

Then its image under $U$ is also a pullback and thus $U(f)$ is a monomorphism in $\mathsf{Set}$ : that is, $f$ is an injective function.

For space reasons, we omit the proof that $G$ preserves pullbacks. Using Lemma 7.1, we can establish the first required property of $G$ .

Lemma 7.2.

The functor $G:\mathsf{CA}\to\mathsf{CA}$ on $\mathsf{CA}$ is finitary.

Proof.

We are going to use the following results:

Fact 1.: The forgetful functor $U\colon\mathsf{CA}\to\mathsf{Set}$ creates directed colimits.
Fact 2.: Let $\mathsf{C}$ be a category equipped with a functor $U\colon\mathsf{C}\to\mathsf{S}$ that creates – hence, preserves and reflects – directed colimits. Let $G\colon\mathsf{C}\to\mathsf{C}$ be a lifting of an endofunctor $H\colon\mathsf{S}\to\mathsf{S}$ , i.e., $U\circ G=H\circ U$ . Then, if $H$ preserves directed colimits, so does $G$ .

In our situation, $G$ is defined in Eq. 5.2, $\mathsf{C}=\mathsf{CA}$ , and $\mathsf{S}=\mathsf{Set}$ . The proof of Fact 1 is routine, and similar to that of [1, Remark 3.4 (vii).(4)].

Let us briefly establish Fact 2. Let $D\colon(I,\leq)\to\mathsf{C}$ be a directed diagram in $\mathsf{C}$ , and let $(d_{i}\colon Di\to Y)_{i\in I}$ be a colimiting cocone for $D$ . We want to show that $(G(d_{i})\colon GDi\to GY)_{i\in I}$ is a colimiting cocone for $G\circ D$ . Since $U$ reflects colimits, it suffices to show that $(UG(d_{i})\colon UGDi\to UGY)_{i\in I}$ is a colimiting cocone for $U\circ G\circ D$ . To this end, consider the directed diagram $U\circ D\colon(I,\leq)\to\mathsf{S}$ . Since $U$ preserves directed colimits, $(U(d_{i})\colon UDi\to UY)_{i\in I}$ is a colimiting cocone for $U\circ D$ . Now, since $H$ is finitary, i.e., it preserves directed colimits, $(HU(d_{i})\colon HUDi\to HUY)_{i\in I}$ is a colimiting cocone of the directed diagram $H\circ U\circ D$ . But $H\circ U=U\circ G$ , so we can conclude that $(UG(d_{i})\colon UGDi\to UGY)_{i\in I}$ is a colimiting cocone of the directed diagram $U\circ G\circ D$ , as desired.

We can now proceed with the proof of the lemma. Recall from Remark 5.6 that $G$ (from Eq. 5.2) is a lifting of the endofunctor $H$ . The functor $H$ is finitary because for any set $X$ , and any function $f\in HX$ , there is the finite set $Z=\{x\in X\mid\exists a\in A\exists r>0\text{ such that }f(a)=(r,x)\}$ with $f\in HZ$ . By Fact 1, the forgetful functor $U\colon\mathsf{CA}\to\mathsf{Set}$ creates directed colimits. Thus, the conditions of Fact 2 are satisfied, and we may conclude that $G$ is finitary. $\hfill\blacktriangleleft$

Lemma 7.3.

$G$ preserves surjective affine maps.

Proof.

Let $h\colon X\to Y$ be a surjective affine map. Consider $G(h)\colon GX\to GY$ . For $a\in A$ , we have $G(h)(g)(a)(\bot)=\bot$ and $G(h)(g)(a)(r\cdot x)=r\cdot h(x)$ .

Take $f\in GY$ . For each $y\in Y$ , denote by $x_{y}$ an element of $X$ with $y=h(x_{y})$ . Such exists since $h$ is surjective. We define $g\colon A\to X_{\bot}$ as follows. For $a\in A$ , if $f(a)=\bot$ , set $g(a)=\bot$ and if $f(a)=r\cdot y$ , set $g(a)=r\cdot x_{y}$ . Then $g\in GX$ and $G(h)(g)=f$ . $\hfill\blacktriangleleft$

The most interesting point in this section is the properness of $G$ (see Definition 7.6). In order to verify that $G$ is proper, we need a few lemmas regarding bisimilarity and behavioural equivalence for $G$ -coalgebras.

Lemma 7.4.

Let $(X,\gamma)$ be a $G$ -coalgebra on $\mathsf{CA}$ . Then bisimilarity (the largest bisimulation) on $(X,c)$ coincides with behavioural equivalence, which in turn coincides with the final coalgebra semantics.

Proof.

Behavioural equivalence always coincides with the final coalgebra semantics if the functor admits a final coalgebra, which is the case for our functor $G$ on $\mathsf{CA}$ .

$\mathsf{CA}$ is complete and cocomplete [2, § 9.3, Prop. 4] and the functor $G$ preserves (weak) pullbacks by Lemma 7.1. So $\mathsf{CA}$ satisfies the requirements of [30, Theorem 4.1]. As a consequence: (1) every bisimulation is contained in a kernel bisimulation, and hence bisimilar states are behaviourally equivalent, and (2) every kernel bisimulation is a bisimulation, yielding that behaviourally equivalent states are bisimilar. $\hfill\blacktriangleleft$

We need one more lemma that characterises bisimilarity for $G$ in concrete terms. The proof follows directly from the definition of bisimulation.

Lemma 7.5.

Let $(X,\gamma)$ and $(Y,\vartheta)$ be $G$ -coalgebras. Let $R\subseteq X\times Y$ be a subalgebra of $X\times Y$ . Then $R$ is a bisimulation between $(X,\gamma)$ and $(Y,\vartheta)$ if and only if the following holds: whenever $a\in A$ and $(x,y)\in R$ , $\mbox{\sf mass}_{\gamma}(a,x)=\mbox{\sf mass}_{\vartheta}(a,y)$ , and if $\mbox{\sf mass}_{\gamma}(a,x)=\mbox{\sf mass}_{\vartheta}(a,y)\neq 0$ , then $R$ contains $(\mbox{\sf next}_{\gamma}(a,x),\mbox{\sf next}_{\vartheta}(a,y))$ .

Without further ado, let us now proceed with the proof that $G$ is a proper functor, in the following sense.

Definition 7.6.

Let $T$ be a finitary monad on $\mathsf{Set}$ and write $\mathsf{Set}^{T}$ for the Eilenberg-Moore category of $T$ . A zig-zag in $\mbox{\sf Coalg}_{\mathsf{Set}^{T}}(F)$ is a diagram of the shape

(7.1)

Write $\eta$ for the unit of $T$ . The zig-zag above relates $x\in X$ with $y\in Y$ , written $x\sim y$ , if there exist elements $z_{2k}\in Z_{2k}$ , $k=1,\ldots,n-1$ , with (setting $z_{0}=x$ and $z_{2n}=y$ )

f_{2k}(z_{2k})=f_{2k-1}(z_{2k-2}),\quad k=1,\ldots,n

The endofunctor $F$ is said to be proper if the following statement holds: for any pair of ffg $F$ -coalgebras $(T(X),c^{X})$ and $(T(Y),c^{Y})$ and any two elements $x\in X$ and $y\in Y$ with $\eta_{X}(x)\sim\eta_{Y}(y)$ , there exists a zig-zag in $\mbox{\sf Coalg}_{\mathsf{Set}^{T}}(F)$ entirely consisting of ffg $F$ -coalgebras that relates $\eta_{X}(x)$ with $\eta_{Y}(y)$ . We may call such a zig-zag an ffg zig-zag.

Theorem 7.7.

The functor $G:\mathsf{CA}\to\mathsf{CA}$ is proper.

Proof.

Consider two ffg $G$ -coalgebras $({\mathcal{D}}(X),\partial_{\beta})$ and $({\mathcal{D}}(Y),\partial_{\vartheta})$ , with behaviourally equivalent states $\varphi\in{\mathcal{D}}(X)$ and $\psi\in{\mathcal{D}}(Y)$ . We need to relate $\varphi$ and $\psi$ with a suitable, ffg, zig-zag. We are going to use bisimilarity $B$ on the coproduct coalgebra²²2Left adjoints preserve colimits, so indeed the coproduct of free convex algebras is given by the formula ${\mathcal{D}}(X)+{\mathcal{D}}(Y)\cong{\mathcal{D}}(X+Y)$ , where the “ $+$ ” on the left hand side is the coproduct in $\mathsf{CA}$ . $({\mathcal{D}}(X),\partial_{\beta})+({\mathcal{D}}(Y),\partial_{\vartheta})% \cong({\mathcal{D}}(X+Y),\partial_{\beta}+\partial_{\vartheta})$ .

where $\iota_{1},\iota_{2}$ denote the coproduct injections. It remains to show that $B$ is finitely generated as a subalgebra of the product $\mathsf{CA}$ , ${\mathcal{D}}(X+Y)\times{\mathcal{D}}(X+Y)$ . This follows from results below, using an analytic-algebraic characterization of finitely generated congruences (kernels of convex algebra homomorphisms) of finitely generated convex algebras.

In more detail, note that we can identify any ffg algebra ${\mathcal{D}}(X)$ with the simplex in the vector space $\mathbb{R}^{X}$ . This can be done by seeing each Dirac delta $1\cdot x$ as a unit vector in $\mathbb{R}^{X}$ . Every congruence relation $R\subseteq{\mathcal{D}}(X)\times{\mathcal{D}}(X)$ of convex algebras is a subalgebra of ${\mathcal{D}}(X)\times{\mathcal{D}}(X)$ , and so by extension can be identified with a (convex) subset of $\mathbb{R}^{X}\times\mathbb{R}^{X}\cong\mathbb{R}^{2X}$ . In particular, our $B$ can be identified with a convex subset of $\mathbb{R}^{2(X+Y)}$ . As turns out, $B$ is finitely generated as a subalgebra if and only if $B$ is topologically closed in $\mathbb{R}^{2(X+Y)}$ . The following theorem is a direct consequence of Sokolova-Woracek [27, Proposition 5.9].

Theorem 7.8.

Let $R\subseteq\mathbb{R}^{2X}$ be a congruence on the ffg convex algebra ${\mathcal{D}}(X)\subseteq\mathbb{R}^{X}$ . Then $R$ is finitely generated as a subalgebra if and only if it is topologically closed (closed under limits of Cauchy sequences).

Lemma 7.9.

Let $({\mathcal{D}}(X),\partial_{\beta})$ be a $G$ -coalgebra. Then for any $a\in A$ , the maps $\partial_{\beta}(-)(a)$ and $\mbox{\sf mass}_{\beta}(a,-)$ are restrictions of $\mathbb{R}$ -linear maps $\mathbb{R}^{X}\to\mathbb{R}^{X+1}$ and $\mathbb{R}^{X}\to\mathbb{R}$ respectively.

Proof.

Recall that we think of the Dirac distributions $1\cdot x$ as the basis vectors of $\mathbb{R}^{X}$ . We additionally have the unit vector $1\cdot\bot$ in $\mathbb{R}^{X+1}$ . For $x\in X$ , write

\partial_{\beta}(x)(a)=\sum_{y\in X}r_{xy}\cdot y

and $r_{x\bot}=1-\sum_{y\in X}r_{xy}$ . Define the matrix $M$ by

M=\begin{bmatrix}r_{x\xi}\leavevmode\nobreak\ \big{|}\leavevmode\nobreak\ x\in X% \text{ and }\xi\in X\cup\{\bot\}\end{bmatrix}

indexed by $X\times(X\cup\{\bot\})$ . A quick calculation verifies that indeed, for $\theta\in{\mathcal{D}}(X)$ , $\partial_{\beta}(\theta)(a)=M\theta$ by linear extension. Of course, here we are thinking of $\theta=\sum_{x\in X}q_{x}\cdot x$ as the column vector $[q_{x}\mid x\in X]$ .

Similarly, define the row matrix $N=[1\mid x\in X]$ of $1$ ’s. Then for $\theta=\sum_{x\in X}q_{x}\cdot x$ ,

N\theta=\begin{bmatrix}1&\cdots&1\end{bmatrix}[q_{x}\mid x\in X]=\sum_{x\in X}% q_{x}

We therefore have $\mbox{\sf mass}_{\beta}(a,\theta)=NM\theta$ . Thus, both $\partial_{\beta}(-)(a)$ and $\mbox{\sf mass}_{\beta}(a,-)$ are restrictions of linear functions. $\hfill\blacktriangleleft$

Corollary 7.10.

Let $({\mathcal{D}}(X),\partial_{\beta})$ be a $G$ -coalgebra. Then for any $a\in A$ , the maps $\partial_{\beta}(-)(a)$ and $\mbox{\sf mass}_{\beta}(a,-)$ are continuous.

Proof.

Follows directly from Lemma 7.9 and that $\mathbb{R}^{X}$ , $\mathbb{R}^{X+1}$ , and $\mathbb{R}$ are finite dimensional. $\hfill\blacktriangleleft$

Theorem 7.11.

Let $({\mathcal{D}}(X),\partial_{\beta})$ and $({\mathcal{D}}(Y),\partial_{\vartheta})$ be free finitely generated $G$ -coalgebras. Let $(B,\ell)$ be the largest bisimulation between ${\mathcal{D}}(X)$ and ${\mathcal{D}}(Y)$ , and regard $B$ as a subset of ${\mathcal{D}}(X+Y)\times{\mathcal{D}}(X+Y)\subseteq\mathbb{R}^{2(X+Y)}$ . Then $B$ is a closed set and thus is finitely generated as a subalgebra.

Proof.

We show that the topological closure $\overline{B}$ of $B\subseteq\mathbb{R}^{2(X+Y)}$ is a bisimulation between $({\mathcal{D}}(X),\partial_{\beta})$ and $({\mathcal{D}}(Y),\partial_{\vartheta})$ . Since $B$ is the largest bisimulation, $B\subseteq\overline{B}\subseteq B$ .

We appeal to Lemma 7.5: Let $(\theta,\psi)\in\overline{B}$ . Then there is a Cauchy sequence $(\theta_{i},\psi_{i})_{i\in\mathbb{N}}$ such that $(\theta_{i},\psi_{i})\to(\theta,\psi)$ as $i\to\infty$ . This, in particular, means that $\theta_{i}\to\theta$ and $\psi_{i}\to\psi$ in the product topology. Now, for $a\in A$ ,

$\displaystyle\mbox{\sf mass}_{\beta}(a,\theta)$	$\displaystyle=\mbox{\sf mass}_{\beta}(a,\lim\theta_{i})$
	$\displaystyle=\lim\mbox{\sf mass}_{\beta}(a,\theta_{i})$	(Corollary 7.10)
	$\displaystyle=\lim\mbox{\sf mass}_{\vartheta}(a,\psi_{i})$	(Lemma 7.5)
	$\displaystyle=\mbox{\sf mass}_{\vartheta}(a,\lim\psi_{i})$	(Corollary 7.10)
	$\displaystyle=\mbox{\sf mass}_{\vartheta}(a,\psi)$

This verifies the first condition. To verify the second, suppose that $\mbox{\sf mass}_{\beta}(a,\theta)=\mbox{\sf mass}_{\vartheta}(a,\psi)\neq 0$ . Then there is an $N>0$ such that for all $i>N$ , $\mbox{\sf mass}_{\beta}(a,\theta_{i})=\mbox{\sf mass}_{\vartheta}(a,\psi_{i})>0$ . This allows for the following computation:

\mbox{\sf next}_{\beta}(a,\theta)=\frac{\partial_{\beta}(\theta)(a)}{\mbox{\sf mass% }_{\beta}(a,\theta)}\overset{(*)}{=}\lim\frac{\partial_{\beta}(\theta_{i})(a)}% {\mbox{\sf mass}_{\beta}(a,\theta_{i})}=\lim\mbox{\sf next}_{\beta}(a,\theta_{% i})

and similarly for $\psi$ . Above, the step tagged (*) is due to the fact that a product of continuous functions is continuous on the intersection of their domain, which in this case contains all of the $\theta_{i}$ as well as $\theta$ . Simply put, we use a known rule for computing limits of sequences of fractions: The limit of the pointwise-fractions of two sequences is the quotient of the two limits, given that the denominator sequence has non-zero limit. This tells us that

(\mbox{\sf next}_{\beta}(a,\theta),\mbox{\sf next}_{\vartheta}(a,\psi))=\lim(% \mbox{\sf next}_{\beta}(a,\theta_{i}),\mbox{\sf next}_{\vartheta}(a,\psi_{i}))% \in\overline{B}

By Lemma 7.5, $\overline{B}$ is a bisimulation, as desired. $\hfill\blacktriangleleft$

At long last, we complete the proof of Theorem 7.7 with an appeal to Theorem 7.11. $\hfill\blacktriangleleft$

Recap of the proof of completeness, Theorem 3.6

We have taken the approach outlined in Section 4 to showing that the axioms in Fig. 1 are complete with respect to the stream semantics of probabilistic process terms (Proposition 2.3). In Step 1, we observed that the semantics map $\left\llbracket{-}\right\rrbracket$ coincides with determinized stream semantics $\llparenthesis{-}\rrparenthesis$ (Theorem 5.13), and that in particular this meant that the final $G$ -coalgebra homomorphism $\partial^{\dagger}\colon(\mathsf{PTerm}/{\equiv},\partial)\to(\text{\sf Prob}(% A^{\omega}),\zeta)$ satisfies $\left\llbracket{e}\right\rrbracket=\partial^{\dagger}([e])$ for each $e\in\mathsf{PTerm}$ (Theorem 6.3). Thus, it suffices to show that $\partial^{\dagger}$ is injective. To this end, we observed in Section 4 that it suffices to construct a left inverse $k$ to $q$ in the diagram below.

(7.2)

The left inverse $k$ in (7.2) exists if $(\mathsf{PTerm}/{\equiv},\partial^{\dagger})$ is the final locally fg $G$ -coalgebra. In Step 2, we saw that $(\mathsf{PTerm}/{\equiv},\partial^{\dagger})$ satisfies a slightly weaker universal property, that every ffg $G$ -coalgebra admits a unique coalgebra homomorphism into it (Theorem 6.9). In Step 3, we verified the hypotheses of Theorem 4.4, in particular Theorem 7.7, which tells us that in fact, $(\mathsf{PTerm}/{\equiv},\partial^{\dagger})$ is the final locally fg coalgebra, as desired. This finishes the proof of completeness, Theorem 3.6.

8 Discussion and Related Work

We present the first sound and complete axiomatization of infinite trace semantics for generative probabilistic transition systems, settling a recent conjecture of Schmid, Noquez, and Moss [21]. Our completeness theorem on infinite traces is a new direction in a series of coalgebraic completeness theorems on finite trace semantics for probabilistic process calculi [25, 18], thus expanding the scope of this line of work. Our approach is categorical, and we build on recent results on proper functors over convex sets. In our proof, we use an analytic-algebraic result about convex congruences to show properness of $G$ . The particular functor which we prove to be proper has not been studied before, and the properness proof technique of [28] does not apply to it, but remarkably we could use a result concerning the geometry of convex congruences due to Sokolova and Woracek [27].

We provide a characterization of infinite traces as the final coalgebra semantics of a functor over convex algebras. Infinite traces have been studied in the context of semantics of (variants of GPTS) before: via a largest homomorphism in the (order enriched) Kleisli category of the Giry monad [32] due to Urabe and Hasuo, via a greatest fixpoint in a category of generalised relations [4] due to Cîrstea, as a final coalgebra on a free positive convex algebra (a convex algebra with a distinguished element, i.e., in the Kleisli category of the subdistribution monad) due to Kerstan and König [9], and as a subcoalgebra of the final Moore automaton on a positive convex algebra (in the Eilenberg-Moore category of the subdistribution monad) due to Goy and Rot [5, 6]. We offer a fourth characterization as a final coalgebra semantics for a new functor on convex algebras (i.e., in the Eilenberg-Moore category of the finite probability distribution monad) in Section 5. It is also the final coalgebra of a set functor.

In the future, we want to explore whether the argument we provided for properness generalizes to other endofunctors on $\mathsf{CA}$ and to endofunctors on the category of positive convex algebras used in [25, 18]. We would like to expand our completeness theorem to incorporate hypotheses, especially in the context [21] where actions are interpreted concretely as contractions on a space: If the space and the contractions are fixed, the actions might satisfy additional relations. More speculatively, it might be interesting to also go in the opposite direction: Given a set of hypotheses, can one construct a canonical space and a contraction interpretation of the actions that satisfies the hypotheses? We would also like to consider different syntax for specifying LMCs and stream measures, such as the so-called formal language of recursion [7], which connects nicely to iterative algebra. Orthogonally, we would like to explore axiomatizations of behavioural distances, in the style of quantitative equational theories [12]. Last but not least, we would like to explore unifying the results of Silva and Sokolova [25] with those of this paper.

References

[1] J. Adámek and J. Rosicky. Locally Presentable and Accessible Categories. London Mathematical Society Lecture Note Series. Cambridge University Press, 1994.
[2] M. Barr and Ch. Wells. Toposes, Triples and Theories. Springer, Berlin, 1985. Revised and corrected version available from URL: www.cwru.edu/artsci/math/wells/pub/ttt.html.
[3] F. Bartels, A. Sokolova, and E.P. de Vink. A hierarchy of probabilistic system types. Theoretical Computer Science, 327:3–22, 2004. doi:10.1016/J.TCS.2004.07.019.
[4] Corina Cîrstea. From branching to linear time, coalgebraically. Fundam. Informaticae, 150(3-4):379–406, 2017. doi:10.3233/FI-2017-1474.
[5] Alexandre Goy. Trace semantics via determinization for probabilistic transition systems. CoRR, abs/1802.09084, 2018. arXiv:1802.09084.
[6] Alexandre Goy and Jurriaan Rot. (In)finite trace equivalence of probabilistic transition systems. In Corina Cîrstea, editor, Coalgebraic Methods in Computer Science - 14th IFIP WG 1.3 International Workshop, CMCS 2018, volume 11202 of Lecture Notes in Computer Science, pages 100–121. Springer, 2018. doi:10.1007/978-3-030-00389-0_7.
[7] Antonius J. C. Hurkens, Monica McArthur, Yiannis N. Moschovakis, Lawrence S. Moss, and Glen T. Whitney. The logic of recursive equations. J. Symb. Log., 63(2):451–478, 1998. doi:10.2307/2586843.
[8] Bart Jacobs. A bialgebraic review of deterministic automata, regular expressions and languages. In Kokichi Futatsugi, Jean-Pierre Jouannaud, and José Meseguer, editors, Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, volume 4060 of Lecture Notes in Computer Science, pages 375–404. Springer, 2006. doi:10.1007/11780274_20.
[9] Henning Kerstan and Barbara König. Coalgebraic Trace Semantics for Continuous Probabilistic Transition Systems. Logical Methods in Computer Science, Volume 9, Issue 4, December 2013. doi:10.2168/LMCS-9(4:16)2013.
[10] S. C. Kleene. Representation of events in nerve nets and finite automata. In Claude Shannon and John McCarthy, editors, Automata Studies, pages 3–41. Princeton University Press, Princeton, NJ, 1956.
[11] Kim Guldstrand Larsen and Arne Skou. Bisimulation through probabilistic testing. Inf. Comput., 94(1):1–28, 1991. doi:10.1016/0890-5401(91)90030-6.
[12] Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In 2016 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–10, 2016.
[13] Stefan Milius. A sound and complete calculus for finite stream circuits. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, pages 421–430. IEEE Computer Society, 2010. doi:10.1109/LICS.2010.11.
[14] Stefan Milius. Proper functors and fixed points for finite behaviour. Log. Methods Comput. Sci., 14(3), 2018. doi:10.23638/LMCS-14(3:22)2018.
[15] Robin Milner. A complete inference system for a class of regular behaviours. J. Comput. Syst. Sci., 28(3):439–466, 1984. doi:10.1016/0022-0000(84)90023-0.
[16] Michael O. Rabin. Probabilistic automata. Inf. Control., 6(3):230–245, 1963. doi:10.1016/S0019-9958(63)90290-0.
[17] Alexander Moshe Rabinovich. A complete axiomatisation for trace congruence of finite state behaviors. In Stephen D. Brookes, Michael G. Main, Austin Melton, Michael W. Mislove, and David A. Schmidt, editors, Mathematical Foundations of Programming Semantics, 9th International Conference, New Orleans, LA, USA, April 7-10, 1993, Proceedings, volume 802 of Lecture Notes in Computer Science, pages 530–543. Springer, 1993. doi:10.1007/3-540-58027-1_25.
[18] Wojciech Rozowski and Alexandra Silva. A completeness theorem for probabilistic regular expressions. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024, pages 66:1–66:14. ACM, 2024. doi:10.1145/3661814.3662084.
[19] Walter Rudin. Real and Complex Analysis. McGraw-Hill, 1966.
[20] Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3–80, 2000. doi:10.1016/S0304-3975(00)00056-6.
[21] Todd Schmid, Victoria Noquez, and Lawrence S. Moss. Fractals from regular behaviours. In Paolo Baldan and Valeria de Paiva, editors, 10th Conference on Algebra and Coalgebra in Computer Science, CALCO 2023, June 19-21, 2023, Indiana University Bloomington, IN, USA, volume 270 of LIPIcs, pages 14:1–14:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. Also available at https://arxiv.org/pdf/2306.03894. doi:10.4230/LIPICS.CALCO.2023.14.
[22] Todd Schmid, Jurriaan Rot, and Alexandra Silva. On star expressions and coalgebraic completeness theorems. In Ana Sokolova, editor, Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021, volume 351 of EPTCS, pages 242–259, 2021. doi:10.4204/EPTCS.351.15.
[23] Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Log. Methods Comput. Sci., 9(1), 2013. doi:10.2168/LMCS-9(1:9)2013.
[24] Alexandra Silva, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Non-deterministic kleene coalgebras. Log. Methods Comput. Sci., 6(3), 2010. URL: http://arxiv.org/abs/1007.3769.
[25] Alexandra Silva and Ana Sokolova. Sound and complete axiomatization of trace semantics for probabilistic systems. In Michael W. Mislove and Joël Ouaknine, editors, Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 2011, Pittsburgh, PA, USA, May 25-28, 2011, volume 276 of Electronic Notes in Theoretical Computer Science, pages 291–311. Elsevier, 2011. doi:10.1016/j.entcs.2011.09.027.
[26] A. Sokolova and E.P. de Vink. Probabilistic automata: system types, parallel composition and comparison. In C. Baier, B.R. Haverkort, H. Hermanns, J.-P. Katoen, and M. Siegle, editors, Validation of Stochastic Systems: A Guide to Current Research, pages 1–43. LNCS 2925, 2004. doi:10.1007/978-3-540-24611-4_1.
[27] Ana Sokolova and Harald Woracek. Congruences of convex algebras. Journal of Pure and Applied Algebra, 219(8):3110–3148, 2015. doi:10.1016/j.jpaa.2014.10.005.
[28] Ana Sokolova and Harald Woracek. Proper semirings and proper convex functors. In FoSSaCS 2018, pages 331–347. LNCS 10803, 2018.
[29] Eugene W. Stark and Scott A. Smolka. A complete axiom system for finite-state probabilistic processes. In Gordon D. Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language, and Interaction, Essays in Honour of Robin Milner, pages 571–596. The MIT Press, 2000.
[30] Sam Staton. Relating coalgebraic notions of bisimulation. In CALCO 2009, volume 5728, pages 191–205. LNCS 5728, 2009. doi:10.1007/978-3-642-03741-2_14.
[31] T. Świrszcz. Monadic functors and convexity. Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys., 22:39–42, 1974.
[32] Natsuki Urabe and Ichiro Hasuo. Coalgebraic infinite traces and Kleisli simulations. Log. Methods Comput. Sci., 14(3), 2018. doi:10.23638/LMCS-14(3:15)2018.

[bib.bib1] [1] J. Adámek and J. Rosicky. Locally Presentable and Accessible Categories. London Mathematical Society Lecture Note Series. Cambridge University Press, 1994.

[bib.bib2] [2] M. Barr and Ch. Wells. Toposes, Triples and Theories. Springer, Berlin, 1985. Revised and corrected version available from URL: www.cwru.edu/artsci/math/wells/pub/ttt.html.

[bib.bib3] [3] F. Bartels, A. Sokolova, and E.P. de Vink. A hierarchy of probabilistic system types. Theoretical Computer Science, 327:3–22, 2004. doi:10.1016/J.TCS.2004.07.019.

[bib.bib4] [4] Corina Cîrstea. From branching to linear time, coalgebraically. Fundam. Informaticae, 150(3-4):379–406, 2017. doi:10.3233/FI-2017-1474.

[bib.bib5] [5] Alexandre Goy. Trace semantics via determinization for probabilistic transition systems. CoRR, abs/1802.09084, 2018. arXiv:1802.09084.

[bib.bib6] [6] Alexandre Goy and Jurriaan Rot. (In)finite trace equivalence of probabilistic transition systems. In Corina Cîrstea, editor, Coalgebraic Methods in Computer Science - 14th IFIP WG 1.3 International Workshop, CMCS 2018, volume 11202 of Lecture Notes in Computer Science, pages 100–121. Springer, 2018. doi:10.1007/978-3-030-00389-0_7.

[bib.bib7] [7] Antonius J. C. Hurkens, Monica McArthur, Yiannis N. Moschovakis, Lawrence S. Moss, and Glen T. Whitney. The logic of recursive equations. J. Symb. Log., 63(2):451–478, 1998. doi:10.2307/2586843.

[bib.bib8] [8] Bart Jacobs. A bialgebraic review of deterministic automata, regular expressions and languages. In Kokichi Futatsugi, Jean-Pierre Jouannaud, and José Meseguer, editors, Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, volume 4060 of Lecture Notes in Computer Science, pages 375–404. Springer, 2006. doi:10.1007/11780274_20.

[bib.bib9] [9] Henning Kerstan and Barbara König. Coalgebraic Trace Semantics for Continuous Probabilistic Transition Systems. Logical Methods in Computer Science, Volume 9, Issue 4, December 2013. doi:10.2168/LMCS-9(4:16)2013.

[bib.bib10] [10] S. C. Kleene. Representation of events in nerve nets and finite automata. In Claude Shannon and John McCarthy, editors, Automata Studies, pages 3–41. Princeton University Press, Princeton, NJ, 1956.

[bib.bib11] [11] Kim Guldstrand Larsen and Arne Skou. Bisimulation through probabilistic testing. Inf. Comput., 94(1):1–28, 1991. doi:10.1016/0890-5401(91)90030-6.

[bib.bib12] [12] Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In 2016 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–10, 2016.

[bib.bib13] [13] Stefan Milius. A sound and complete calculus for finite stream circuits. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, pages 421–430. IEEE Computer Society, 2010. doi:10.1109/LICS.2010.11.

[bib.bib14] [14] Stefan Milius. Proper functors and fixed points for finite behaviour. Log. Methods Comput. Sci., 14(3), 2018. doi:10.23638/LMCS-14(3:22)2018.

[bib.bib15] [15] Robin Milner. A complete inference system for a class of regular behaviours. J. Comput. Syst. Sci., 28(3):439–466, 1984. doi:10.1016/0022-0000(84)90023-0.

[bib.bib16] [16] Michael O. Rabin. Probabilistic automata. Inf. Control., 6(3):230–245, 1963. doi:10.1016/S0019-9958(63)90290-0.

[bib.bib17] [17] Alexander Moshe Rabinovich. A complete axiomatisation for trace congruence of finite state behaviors. In Stephen D. Brookes, Michael G. Main, Austin Melton, Michael W. Mislove, and David A. Schmidt, editors, Mathematical Foundations of Programming Semantics, 9th International Conference, New Orleans, LA, USA, April 7-10, 1993, Proceedings, volume 802 of Lecture Notes in Computer Science, pages 530–543. Springer, 1993. doi:10.1007/3-540-58027-1_25.

[bib.bib18] [18] Wojciech Rozowski and Alexandra Silva. A completeness theorem for probabilistic regular expressions. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024, pages 66:1–66:14. ACM, 2024. doi:10.1145/3661814.3662084.

[bib.bib19] [19] Walter Rudin. Real and Complex Analysis. McGraw-Hill, 1966.

[bib.bib20] [20] Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3–80, 2000. doi:10.1016/S0304-3975(00)00056-6.

[bib.bib21] [21] Todd Schmid, Victoria Noquez, and Lawrence S. Moss. Fractals from regular behaviours. In Paolo Baldan and Valeria de Paiva, editors, 10th Conference on Algebra and Coalgebra in Computer Science, CALCO 2023, June 19-21, 2023, Indiana University Bloomington, IN, USA, volume 270 of LIPIcs, pages 14:1–14:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. Also available at https://arxiv.org/pdf/2306.03894. doi:10.4230/LIPICS.CALCO.2023.14.

[bib.bib22] [22] Todd Schmid, Jurriaan Rot, and Alexandra Silva. On star expressions and coalgebraic completeness theorems. In Ana Sokolova, editor, Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021, volume 351 of EPTCS, pages 242–259, 2021. doi:10.4204/EPTCS.351.15.

[bib.bib23] [23] Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Log. Methods Comput. Sci., 9(1), 2013. doi:10.2168/LMCS-9(1:9)2013.

[bib.bib24] [24] Alexandra Silva, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Non-deterministic kleene coalgebras. Log. Methods Comput. Sci., 6(3), 2010. URL: http://arxiv.org/abs/1007.3769.

[bib.bib25] [25] Alexandra Silva and Ana Sokolova. Sound and complete axiomatization of trace semantics for probabilistic systems. In Michael W. Mislove and Joël Ouaknine, editors, Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 2011, Pittsburgh, PA, USA, May 25-28, 2011, volume 276 of Electronic Notes in Theoretical Computer Science, pages 291–311. Elsevier, 2011. doi:10.1016/j.entcs.2011.09.027.

[bib.bib26] [26] A. Sokolova and E.P. de Vink. Probabilistic automata: system types, parallel composition and comparison. In C. Baier, B.R. Haverkort, H. Hermanns, J.-P. Katoen, and M. Siegle, editors, Validation of Stochastic Systems: A Guide to Current Research, pages 1–43. LNCS 2925, 2004. doi:10.1007/978-3-540-24611-4_1.

[bib.bib27] [27] Ana Sokolova and Harald Woracek. Congruences of convex algebras. Journal of Pure and Applied Algebra, 219(8):3110–3148, 2015. doi:10.1016/j.jpaa.2014.10.005.

[bib.bib28] [28] Ana Sokolova and Harald Woracek. Proper semirings and proper convex functors. In FoSSaCS 2018, pages 331–347. LNCS 10803, 2018.

[bib.bib29] [29] Eugene W. Stark and Scott A. Smolka. A complete axiom system for finite-state probabilistic processes. In Gordon D. Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language, and Interaction, Essays in Honour of Robin Milner, pages 571–596. The MIT Press, 2000.

[bib.bib30] [30] Sam Staton. Relating coalgebraic notions of bisimulation. In CALCO 2009, volume 5728, pages 191–205. LNCS 5728, 2009. doi:10.1007/978-3-642-03741-2_14.

[bib.bib31] [31] T. Świrszcz. Monadic functors and convexity. Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys., 22:39–42, 1974.

[bib.bib32] [32] Natsuki Urabe and Ichiro Hasuo. Coalgebraic infinite traces and Kleisli simulations. Log. Methods Comput. Sci., 14(3), 2018. doi:10.23638/LMCS-14(3:15)2018.

A Complete Inference System for Probabilistic Infinite Trace Equivalence

Abstract

Keywords and phrases:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Acknowledgements:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Labelled Markov Chains and Stream Semantics

Labelled Markov chains.

Example 2.1.

Stream semantics.

Definition 2.2.

Proposition 2.3.

LMCs as coalgebras.

Definition 2.4.

Definition 2.5.

Proposition 2.6.

3 Axiomatizing Stream Semantics

A Specification Language for LMCs

Definition 3.1.

Theorem 3.2.

Corollary 3.3.

Example 3.4.

Axioms for stream equivalence

Definition 3.5 (Provable equivalence).

Theorem 3.6 (Completeness).

4 Blueprint for Proving Completeness

Definition 4.1.

Step 1

Step 2

Definition 4.2.

Lemma 4.3.

Step 3

Theorem 4.4.

5 Step 1: Convex (Co)Algebras and the Functor 𝑮

Convex algebras.

Example 5.1.

Free convex algebras.

Adding a fresh element ⊥ to a convex algebra.

Lemma 5.2.

▶ Remark 5.3.

Lemma 5.4.

The functor 𝑮:𝗖𝗔→𝗖𝗔

Proposition 5.5.

▶ Remark 5.6.

A final 𝑮-coalgebra.

Definition 5.7.

▶ Remark 5.8.

Theorem 5.9.

▶ Remark 5.10.

Determinization: Connecting LMCs and 𝑮-coalgebras

Definition 5.11.

Proposition 5.12.

Theorem 5.13.

Proof.

6 Step 2: 𝗣𝗧𝗲𝗿𝗺/≡ as a 𝑮-coalgebra

Defining ∂.

Lemma 6.1.

Lemma 6.2.

Theorem 6.3.

Proof.

Theorem 6.4.

Proof.

Systems of equations from 𝑮-coalgebras and their unique solutions

Definition 6.5.

Theorem 6.6 (Stark-Smolka [29]).

Corollary 6.7.

Lemma 6.8.

Theorem 6.9.

7 Step 3: Properness of 𝑮

Lemma 7.1.

Lemma 7.2.

Proof.

Lemma 7.3.

5 Step 1: Convex (Co)Algebras and the Functor $𝑮$

Adding a fresh element $\bot$ to a convex algebra.

$\blacktriangleright$ Remark 5.3.

The functor $G:\mathsf{CA}\to\mathsf{CA}$

$\blacktriangleright$ Remark 5.6.

A final $𝑮$ -coalgebra.

$\blacktriangleright$ Remark 5.8.

$\blacktriangleright$ Remark 5.10.

Determinization: Connecting LMCs and $𝑮$ -coalgebras

6 Step 2: $\mathsf{PTerm}/{\equiv}$ as a $𝑮$ -coalgebra

Defining $\partial$ .

Systems of equations from $𝑮$ -coalgebras and their unique solutions

7 Step 3: Properness of $𝑮$