5 papers
A Decision Procedure for Probabilistic Kleene Algebra with Angelic Nondeterminism
Shawn Ong, Dexter Kozen
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).
StacKAT: Infinite State Network Verification
Jules Jacobs, Nate Foster, Tobias Kappé +4
We develop StacKAT, a network verification language featuring loops, finite state variables, nondeterminism, and - most importantly - access to a stack with accompanying push and p…
Probability and Angelic Nondeterminism with Multiset Semantics
Shawn Ong, Stephanie Ma, Dexter Kozen
We introduce a version of probabilistic Kleene algebra with angelic nondeterminism and a corresponding class of automata. Our approach implements semantics via distributions over m…
Joint Distributions in Probabilistic Semantics
Dexter Kozen, Alexandra Silva, Erik Voogd
Various categories have been proposed as targets for the denotational semantics of higher-order probabilistic programming languages. One such proposal involves joint probability di…
A Demonic Outcome Logic for Randomized Nondeterminism
Noam Zilberstein, Dexter Kozen, Alexandra Silva +1
Programs increasingly rely on randomization in applications such as cryptography and machine learning. Analyzing randomized programs has been a fruitful research direction, but the…