2023/11/12 by Kevin Batz, Tom Jannik Biskup, Batz, Kevin +5 · 3 citations
Computer Science · Mathematics · #Bayesian Modeling and Causal Inference #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL) #Statistical Methods in Clinical Trials
paper · pdf · doi:10.48550/arxiv.2311.06889
openalex publication_date 2023/11/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.