Termination in Convex Sets of Distributions

TL;DR

This paper investigates how to extend convex algebras, which model probabilistic systems, by a single point to represent termination, providing a complete classification of such extensions for specific algebra classes.

Contribution

It offers a comprehensive description of all possible single-point extensions of convex algebras used in probabilistic system modeling, including a unique functorial extension.

Findings

Full classification of extensions for convex subsets of a fixed vector space.

Complete description of extensions for free convex algebras.

Identification of a unique functorial 'black-hole' extension.

Abstract

Convex algebras, also called (semi)convex sets, are at the heart of modelling probabilistic systems including probabilistic automata. Abstractly, they are the Eilenberg-Moore algebras of the finitely supported distribution monad. Concretely, they have been studied for decades within algebra and convex geometry. In this paper we study the problem of extending a convex algebra by a single point. Such extensions enable the modelling of termination in probabilistic systems. We provide a full description of all possible extensions for a particular class of convex algebras: For a fixed convex subset $D$ of a vector space satisfying additional technical condition, we consider the algebra of convex subsets of $D$. This class contains the convex algebras of convex subsets of distributions, modelling (nondeterministic) probabilistic automata. We also provide a full description of all possible extensions for the class of free convex algebras, modelling fully probabilistic systems. Finally, we show that there is a unique functorial extension, the so-called black-hole extension.