A Demonic Outcome Logic for Randomized Nondeterminism

Abstract

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.

References in corpus (7)

• Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
• Mixed powerdomains for probability and nondeterminism
• A Separation Logic for Concurrent Randomized Programs
• Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
• Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
• Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
• The Theory of Traces for Systems with Nondeterminism, Probability, and Termination

Cited by in corpus (2)

• Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
• Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects