Verification and refutation of probabilistic specifications via games. (English) Zbl 1248.68333
Kannan, Ravi (ed.) et al., IARCS annual conference on foundations of software technology and theoretical computer science (FSTTCS 2009), December 15–17, 2009, Kanpur, India. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-13-2). LIPIcs – Leibniz International Proceedings in Informatics 4, 251-262, electronic only (2009).
Summary: We develop an abstraction-based framework to check probabilistic specifications of Markov decision processes (MDPs) using the stochastic two-player game abstractions (i.e. “games”) developed by Kwiatkowska et al. as a foundation. We define an abstraction preorder for these game abstractions which enables us to identify many new game abstractions for each MDP – ranging from compact and imprecise to complex and precise. This added ability to trade precision for efficiency is crucial for scalable software model checking, as precise abstractions are expensive to construct in practice. Furthermore, we develop a four-valued probabilistic computation tree logic (PCTL) semantics for game abstractions. Together, the preorder and PCTL semantics comprise a powerful verification and refutation framework for arbitrary PCTL properties of MDPs.
For the entire collection see [Zbl 1213.68045].
For the entire collection see [Zbl 1213.68045].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 91A15 | Stochastic games, stochastic differential games |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
| 03B45 | Modal logic (including the logic of norms) |
| 03B48 | Probability and inductive logic |
