Reference. Denotational Semantics for Probabilistic and Concurrent Programs
We develop a denotational model for probabilistic and concurrent imperative programs, a class of programs with standard control flow via conditionals and while-loops, as well as probabilistic actions and parallel composition. Whereas semantics for concurrent or randomized programs in isolation is well studied, their combination has not been thoroughly explored and presents unique challenges. The crux of the problem is that interactions between control flow, probabilistic actions, and concurrent execution cannot be captured by straightforward generalizations of prior work on pomsets and convex languages, prominent models for those effects, individually. Our model has good domain theoretic properties, important for semantics of unbounded loops. We also prove two adequacy theorems, showing that the model subsumes typical powerdomain semantics for concurrency and convex powerdomain semantics for probabilistic nondeterminism.
Cite
Cited by (2)
Oblivious Probabilistic Outcome Logic: Verifying Probabilistic Programs with an Oblivious Adversary chen-2026-oblivious
In the context of probabilistic programs, an oblivious adversary resolves nondeterminism without seeing the outcomes of random draws. Obliviousness is a common assumption in online algorithms and distributed protocols, but the complex interaction between random draws and adversarial choices makes it challenging to reason about correctness. While there has been significant progress toward reasoning about programs that combine randomization with nondeterminism, most of the work has focused on the adaptive model, whose omniscient view of program state is too powerful to establish correctness for certain classes of programs. We introduce Oblivious Probabilistic Outcome Logic (opOL), a new logic for reasoning about probabilistic programs with nondeterminism controlled by an oblivious adversary. Building on Outcome Logic and Probabilistic Separation Logic, opOL models adversarial choice as a resource and uses probabilistic independence to ensure that random outcomes are hidden from the adversary. The opOL proof system provides expressive and compositional rules for case analysis on both random and nondeterministic outcomes, and for proving almost-sure termination. Expressivity is tested through several case studies, including a paging algorithm and a leader election protocol. The opOL metatheory and case studies are mechanized in Lean 4.
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants zilberstein-2026-probabilistic
Although randomization has long been used in distributed computing, formal methods for reasoning aboutprobabilistic concurrent programs have lagged behind. No existing program logics can express specificationsabout the full distributions of outcomes resulting from programs that are both probabilistic and concurrent. To address this, we introduce Probabilistic Concurrent Outcome Logic ( pcOL ), which incorporates ideas fromconcurrent and probabilistic separation logics into Outcome Logic to introduce new compositional reasoningprinciples. At its core, pcOL reinterprets the rules of Concurrent Separation Logic in a setting where separationmodels probabilistic independence, so as to compositionally describe joint distributions over variables inconcurrent threads. Reasoning about outcomes also proves crucial, as case analysis is often necessary to deriveprecise information about threads that rely on randomized shared state. We demonstrate pcOL on a variety ofexamples, including to prove almost sure termination of unbounded loops.
Cites 73 works (3 here)
With notes (3)
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants zilberstein-2026-probabilistic
Although randomization has long been used in distributed computing, formal methods for reasoning aboutprobabilistic concurrent programs have lagged behind. No existing program logics can express specificationsabout the full distributions of outcomes resulting from programs that are both probabilistic and concurrent. To address this, we introduce Probabilistic Concurrent Outcome Logic ( pcOL ), which incorporates ideas fromconcurrent and probabilistic separation logics into Outcome Logic to introduce new compositional reasoningprinciples. At its core, pcOL reinterprets the rules of Concurrent Separation Logic in a setting where separationmodels probabilistic independence, so as to compositionally describe joint distributions over variables inconcurrent threads. Reasoning about outcomes also proves crucial, as case analysis is often necessary to deriveprecise information about threads that rely on randomized shared state. We demonstrate pcOL on a variety ofexamples, including to prove almost sure termination of unbounded loops.
A Demonic Outcome Logic for Randomized Nondeterminism zilberstein-2025-a
Programs increasingly rely on randomization in applications such as cryptography and machine learning. Analyzing randomized programs has been a fruitful research direction, but there is a gap when programs also exploit nondeterminism(for concurrency, efficiency, or algorithmic design). In this paper, we introduce Demonic Outcome Logic for reasoning about programs that exploit both randomization and nondeterminism. The logic includes several novel features, such as reasoning about multiple executions in tandem and manipulating pre- and postconditions using familiar equational laws—including the distributive law of probabilistic choices over nondeterministic ones. We also give rules for loops that both establish termination and quantify the distribution of final outcomes from a single premise. We illustrate the reasoning capabilities of Demonic Outcome Logic through several case studies, including the Monty Hall problem, an adversarial protocol for simulating fair coins, and a heuristic based probabilistic SAT solver.
Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning zilberstein-2023-outcome
Program logics for bug-finding (such as the recently introduced Incorrectness Logic) have framed correctness and incorrectness as dual concepts requiring different logical foundations. In this paper, we argue that a single unified theory can be used for both correctness and incorrectness reasoning. We present Outcome Logic (OL), a novel generalization of Hoare Logic that is both monadic (to capture computational effects) and monoidal (to reason about outcomes and reachability). OL expresses true positive bugs, while retaining correctness reasoning abilities as well. To formalize the applicability of OL to both correctness and incorrectness, we prove that any false OL specification can be disproven in OL itself. We also use our framework to reason about new types of incorrectness in nondeterministic and probabilistic programs. Given these advances, we advocate for OL as a new foundational theory of correctness and incorrectness.
External (70)
- Denotational Semantics for Probabilistic and Concurrent Programs (Full Version) (2025)
- Branching pomsets: Design, expressiveness and applications to choreographies (2024)
- Multisets and distributions (2024)
- An adequacy theorem between mixed powerdomains and probabilistic concurrency (2024)
- Outcome separation logic: Local reasoning for correctness and incorrectness with computational effects (2024)
- Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity (2023)
- Realisability of Branching Pomsets (2022)
- Branching Pomsets for Choreographies (2022)
- Towards Concurrent Quantitative Separation Logic (2022)
- Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases (2021)
- From Multisets over Distributions to Distributions over Multisets (2021)
- Pomsets with preconditions: a simple model of relaxed memory (2020)
- Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness (2020)
- Monad Composition via Preservation of Algebras (2020)
- On the Non-Compositionality of Monads via Distributive Laws (2020)
- A Separation Logic for Concurrent Randomized Programs (2019)
- No-Go Theorems for Distributive Laws (2019)
- An Assertion-Based Program Logic for Probabilistic Programs (2018)
- A Denotational Semantics for SPARC TSO (2018)
- Verifying Concurrent Randomized Algorithms (2018)
- Mixed powerdomains for probability and nondeterminism (2017)
- Concurrent Kleene algebra with tests and branching automata (2016)
- Completeness Theorems for Bi-Kleene Algebras and Series-Parallel Rational Pomset Languages (2014)
- Probabilistic and Quantum Event Structures (2014)
- Concurrent Kleene Algebra and its Foundations (2011)
- Semantic domains for combining probability and non-determinism (2009)
- Coalgebraic trace semantics for combined possibilitistic and probabilistic systems (2008)
- Probabilistic π-Calculus and Event Structures (2007)
- Distributing probability over non-determinism (2006)
- Abstraction, Refinement and Proof for Probabilistic Systems (2005)
- A semantics for concurrent separation logic (2004)
- Axioms for probability and non-determinism (2004)
- Probabilistic event structures and domains (2004)
- Probability, Nondeterminism and Concurrency: Two Denotational Models for Probabilistic Computation (2003)
- Traces, Pomsets, Fairness and Full Abstraction for Communicating Processes (2002)
- The powerdomain of indexed valuations (2002)
- Nondeterminism and probabilistic choice: Obeying the laws (2000)
- Convex power constructions for continuous d-cones (2000)
- Verifying Probabilistic Programs Using a Hoare like Logic (1999)
- Continuous D-cones: convexity and powerdomain constructions (1999)
- Probabilistic models for the guarded command language (1997)
- Quantitative and Qualitative Extensions of Event Structures (1996)
- Probabilistic Predicate Transformers (1996)
- Refinement-oriented probability for CSP (1996)
- Non-determinism in Functional Languages (1992)
- Metric pomset semantics for a concurrent language with recursion (1990)
- Pomset semantics for true concurrency with synchronization and recursion (1989)
- The equational theory of pomsets (1988)
- Applications of compactness in the smyth powerdomain of streams (1988)
- Countable nondeterminism and random assignment (1986)
- Modeling concurrency with partial orders (1986)
- Finite approximation of spaces (1986)
- Termination of probabilistic concurrent program (1983)
- The choice coordination problem (1982)
- On Partial Languages (1981)
- On the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem (1981)
- Semantics of unbounded nondeterminism (1980)
- N-process synchronization by 4.log2n-valued shared variable (1980)
- Semantics of probabilistic programs (1979)
- Counting large numbers of events in small registers (1978)
- Power domains (1978)
- Proving the correctness of multiprocess programs (1977)
- Chain-complete posets and directed sets with applications (1976)
- A powerdomain construction (1976)
- Semantical Considerations on Floyd-Hoare Logic (1976)
- Hierarchical ordering of sequential processes (1971)
- Toward A Mathematical Semantics For Computer Languages (1971)
- Outline of a Mathematical Theory of Computation (1970)
- An Axiomatic Basis for Computer Programming (1969)
- Assigning Meanings to Programs (1967)