Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Demonic Outcome Logic for Randomized Nondeterminism

Noam Zilberstein, Dexter Kozen, Alexandra Silva, Joseph Tassarotti

TL;DR

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.

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.

A Demonic Outcome Logic for Randomized Nondeterminism

TL;DR

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.

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.

Paper Structure

This paper contains 43 sections, 33 theorems, 122 equations, 10 figures.

Table of Contents

  1. Introduction
  2. An Overview of Demonic, Outcome-Based Reasoning
  3. From Equational Laws to Propositional Reasoning
  4. Program Logics and Compositionality
  5. Reasoning about Loops
  6. Denotational Semantics for Probabilistic Nondeterminism
  7. States, Probability Distributions, and Convex Sets
  8. Semantics of Sequential Commands
  9. Semantics of Loops
  10. Demonic Outcome Logic
  11. Outcome Assertions
  12. Semantics of Triples
  13. Inference Rules
  14. Analyzing Loops
  15. Almost Sure Termination
  16. ...and 28 more sections

Key Result

theorem 1

$\vdash{\color{purple}\boldsymbol\langle} \varphi{\color{purple}\boldsymbol\rangle} ~C~ {\color{purple}\boldsymbol\langle} \psi{\color{purple}\boldsymbol\rangle} \qquad\implies\qquad \vDash{\color{purple}\boldsymbol\langle} \varphi{\color{purple}\boldsymbol\rangle} ~C~ {\color{purple}\boldsymbol\la

Figures (10)

  • Figure 1: Denotational Semantics for programs $\left\llbracket C \right\rrbracket \colon \Sigma \to \mathcal{C}(\Sigma)$, where $\left\llbracket e \right\rrbracket \colon \Sigma\to\mathsf{Val}$ is the interpretation of expressions, defined in the obvious way.
  • Figure 2: Definition of the satisfaction relation $\mathord\vDash \subseteq \mathcal{D}(\Sigma_\bot) \times \mathsf{Prop}$ for Outcome Assertions.
  • Figure 3: Inference rules for non-looping commands in Demonic Outcome Logic.
  • Figure 4: Left: the Monty Hall program. Right: additional program to switch doors
  • Figure 5: Derivation for the $\texttt{\bfseries Game}$ program from \ref{['fig:monty-hall']}.
  • ...and 5 more figures

Theorems & Definitions (40)

  • definition 1: Discrete Probability Distribution
  • definition 2: Convex Sets
  • definition 3: Up-closed Sets
  • definition 4: Semantics of Demonic Outcome Triples
  • theorem 1: Soundness
  • Remark 1: Completeness
  • definition 5: Almost Sure Termination
  • theorem 2
  • lemma 1
  • lemma 2
  • ...and 30 more