Probabilistic Kleene Algebra with Angelic Nondeterminism
summary
Defines a Kleene-style algebra that combines probability with angelic nondeterminism by giving semantics as distributions over multisets to bypass the nonexistence of a distributive law between the powerset and Giry monads. Builds automata with probabilistic, multiset nondeterministic, action and terminal states, proves a full Kleene theorem, gives operational and denotational semantics, a coalgebraic account, and a procedure to translate expressions to automata; constructions are formal and shown to work in the paper.
AI-written summary · about
chapters (10)
- 0:00Introduction to probabilistic Kleene algebra
- 1:05Probability vs nondeterminism
- 2:49Multi-set monads and distributive law
- 4:55Probabilistic automata with angelic nondeterminism
- 6:59Operational semantics via agent model
- 8:45Semantic space assumptions
- 10:54Expressions and fixed-point constructs
- 12:39Kleene theorem for probabilistic automata
- 14:22Closing remarks
- 15:25Q&A
related talks
20mAlgebras for Deterministic Computation are Inherently Incomplete
49mSemantic Foundations for Probabilistic Programming
56mOmnisemantics: Smooth Handling of Nondeterminism (Invited talk)
30mRelatively Complete Verification of Probabilistic Programs
27mThe Relative Monadic Metalanguage
14mAdequacy for Algebraic Effects Revisited
01h 07mAn introduction to synthetic guarded domain theory with applications to probabilistic(…)
19mWell-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny