Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Progr...
summary
Shows a semi-automatic method that synthesizes memoryless deterministic (MD) strategies for probabilistic imperative programs by transforming guards via weakest-precondition reasoning, with a formal claim: for loop-free programs the resulting strategies are correct by construction, and for loops strategy synthesis reduces to user-supplied quantitative loop invariants (so correctness requires those). Uses weakest preexpectations and standard WP-style rules, connects to countably infinite MDP reachability-reward theory, and is mechanizable and validated on several case studies.
AI-written summary · about
chapters (9)
- 0:00Programmatic strategy synthesis intro
- 1:04Modeling gambling game
- 3:14Weakest pre-expectations
- 6:27Non-determinism handling
- 8:35Weakest pre-expectations examples
- 10:19Refining guards for strategies
- 12:29Strategy synthesis for loops
- 13:32Summary and future work
- 14:13Q&A
related talks
24mExact Bayesian Inference for Loopy Probabilistic Programs Using Generating Functions
43mModel Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice
47mBig Ideas in Program Synthesis
38mProgram Synthesis: A Dream Realized?
46mBlueprints for a Universal Reasoning Machine
14mSequential Monte Carlo Program Synthesis with Refinement Proposals
17mModeling Black-Box Components with Probabilistic Synthesis
01h 03mA Personal Viewpoint on Probabilistic Programming