Probability and Angelic Nondeterminism with Multiset Semantics

TL;DR

This paper develops a probabilistic Kleene algebra incorporating angelic nondeterminism, using multiset semantics to establish a comprehensive algebraic and coalgebraic framework with operational and denotational semantics.

Contribution

It introduces a novel probabilistic Kleene algebra with angelic nondeterminism and a multiset-based semantics, overcoming key theoretical barriers and providing a full Kleene theorem and reasoning principles.

Findings

Established a new semantics via distributions over multisets.

Proved a full Kleene theorem for the algebra.

Developed a coalgebraic and operational semantics framework.

Abstract

We introduce a version of probabilistic Kleene algebra with angelic nondeterminism and a corresponding class of automata. Our approach implements semantics via distributions over multisets in order to overcome theoretical barriers arising from the lack of a distributive law between the powerset and Giry monads. We produce a full Kleene theorem and a coalgebraic theory, as well as both operational and denotational semantics and equational reasoning principles.