Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes

Christel BaierChristel Baier, Joachim KleinJoachim Klein, Linda LeuschnerLinda Leuschner, David ParkerDavid Parker, Sascha WunderlichSascha Wunderlich

DOI Link

Christel Baier, Joachim Klein, Linda Leuschner, David Parker, Sascha Wunderlich
Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes
Proc. of the 29th International Conference on Computer Aided Verification (CAV), Part I, volume 10426 of Lecture Notes in Computer Science, 160--180, 2017. Springer

Details
Bibtex

KurzfassungAbstract
Probabilistic model checking provides formal guarantees on quantitative properties such as reliability, performance or risk, so the accuracy of the numerical results that it returns is critical. However, recent results have shown that implementations of value iteration, a widely used iterative numerical method for computing reachability probabilities, can return results that are incorrect by several orders of magnitude. To remedy this, interval iteration, which instead converges simultaneously from both above and below, has been proposed. In this paper, we present interval iteration techniques for computing expected accumulated weights (or costs), a considerably broader class of properties. This relies on an efficient, mainly graph-based method to determine lower and upper bounds for extremal expected accumulated weights. To offset the additional effort of dual convergence, we also propose topological interval iteration, which increases efficiency using a model decomposition into strongly connected components. Finally, we present a detailed experimental evaluation, which highlights inaccuracies in standard benchmarks, rather than just artificial examples, and illustrates the feasibility of our techniques.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-63387-9_8.

@inproceedings{BKLPW2017,
  author    = {Christel Baier and Joachim Klein and Linda Leuschner and David
               Parker and Sascha Wunderlich},
  title     = {Ensuring the Reliability of Your Model Checker: Interval
               Iteration for Markov Decision Processes},
  booktitle = {Proc. of the 29th International Conference on Computer Aided
               Verification (CAV), Part I},
  series    = {Lecture Notes in Computer Science},
  volume    = {10426},
  publisher = {Springer},
  year      = {2017},
  pages     = {160--180},
  doi       = {10.1007/978-3-319-63387-9_8}
}