Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs

arXiv (Cornell University)

Abstract

We consider imperative programs that involve both randomization and pure nondeterminism. The central question is how to find a strategy resolving the pure nondeterminism such that the so-obtained determinized program satisfies a given quantitative specification, i.e., bounds on expected outcomes such as the expected final value of a program variable or the probability to terminate in a given set of states. We show how memoryless and deterministic (MD) strategies can be obtained in a semi-automatic fashion using deductive verification techniques. For loop-free programs, the MD strategies resulting from our weakest precondition-style framework are correct by construction. This extends to loopy programs, provided the loops are equipped with suitable loop invariants - just like in program verification. We show how our technique relates to the well-studied problem of obtaining strategies in countably infinite Markov decision processes with reachability-reward objectives. Finally, we apply our technique to several case studies.

Authors 4

1. Kevin Batz Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , , Germany,

   RWTH Aachen University , Germany TOM JANNIK BISKUP ,

2. Tom Jannik Biskup Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , , Germany,

3. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , , Germany,

   RWTH Aachen University , Germany

4. Tobias Winkler Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , , Germany,

   RWTH Aachen University , Germany