# Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs

arXiv: https://arxiv.org/abs/2311.06889 · HTML: https://mlsanity.com/paper/2311.06889/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 Nov 2023.

## Built on by (most cited first, 1 of 1)

- [dtControl2+varepsilon: Trading Optimality for Explainability in MDPs via Decision Trees](https://mlsanity.com/paper/2607.25925/) (2026)

## Abstract (arXiv)

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.