| Autor: |
Batz, Kevin, Biskup, Tom Jannik, Katoen, Joost-Pieter, Winkler, Tobias |
| Rok vydání: |
2023 |
| Předmět: |
|
| Druh dokumentu: |
Working Paper |
| Popis: |
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. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
