Probability and Angelic Nondeterminism with Multiset Semantics

TL;DR

This work develops a probabilistic Kleene algebra with angelic nondeterminism by modeling choices over finite multisets and employing Beck’s distributive law to couple probability with nondeterminism. Automata and expressions are interpreted over distributions on finite multisets, enabling a full Kleene theorem and a rich denotational and operational semantics along with a supporting metric and verification framework. The authors further establish a coalgebraic semantics, Brzozowski derivatives, and a fundamental theorem to connect syntactic derivatives with semantic behaviors, providing a rigorous foundation for equational reasoning in probabilistic, nondeterministic settings. The approach overcomes classical barriers from distributivity issues and yields a framework with potential for Kleene algebra with tests-style reasoning in probabilistic contexts, with future work on completeness, decidability, and language features. The results contribute a principled, compositional theory for systems combining probability and angelic nondeterminism, with implications for program analysis and verification.

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.

Figures (3)

• Figure 1: Fragment of an automaton
• Figure 2: Examples of automata
• Figure 3: A network security problem

Theorems & Definitions (44)

• proof
• proof
• proof
• proof
• lemma 1
• lemma 2
• proof
• lemma 3
• proof
• lemma 4