A Decision Procedure for Probabilistic Kleene Algebra with Angelic Nondeterminism
Shawn Ong, Dexter Kozen
TL;DR
This paper presents a decision procedure and proof of correctness for the equational theory of probabilistic Kleene algebra with angelic nondeterminism, enabling formal reasoning about probabilistic programs with nondeterministic choices.
Contribution
It introduces a decision procedure for the algebra's equational theory and proves its correctness, advancing formal methods for probabilistic and nondeterministic systems.
Findings
Decision procedure for the algebra's equational theory
Proof of correctness for the decision procedure
Enables formal reasoning about probabilistic nondeterministic programs
Abstract
We give a decision procedure and proof of correctness for the equational theory of probabilistic Kleene algebra with angelic nondeterminism introduced in Ong, Ma, and Kozen (2025).
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsQuantum Mechanics and Applications · Complex Network Analysis Techniques · Opinion Dynamics and Social Influence