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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Standard

Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes. / Baier, Christel ; Klein, Joachim ; Leuschner, Linda ; Parker, David.

Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 22-28, Proceedings. ed. / Rupak Majumdar; Viktor Kunčak. Springer, 2017. p. 160-180 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Harvard

Baier, C, Klein, J, Leuschner, L & Parker, D 2017, Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes. in R Majumdar & V Kunčak (eds), Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 22-28, Proceedings. Lecture Notes in Computer Science, Springer, pp. 160-180, Computer Aided Verification, 29th International Conference, Heidelberg, Germany, 22/07/17. https://doi.org/10.1007/978-3-319-63387-9_8

APA

Baier, C., Klein, J., Leuschner, L., & Parker, D. (2017). Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes. In R. Majumdar, & V. Kunčak (Eds.), Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 22-28, Proceedings (pp. 160-180). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/978-3-319-63387-9_8

Vancouver

Baier C, Klein J, Leuschner L, Parker D. Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes. In Majumdar R, Kunčak V, editors, Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 22-28, Proceedings. Springer. 2017. p. 160-180. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-63387-9_8

Author

Baier, Christel ; Klein, Joachim ; Leuschner, Linda ; Parker, David. / Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes. Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 22-28, Proceedings. editor / Rupak Majumdar ; Viktor Kunčak. Springer, 2017. pp. 160-180 (Lecture Notes in Computer Science).

Bibtex

@inproceedings{bc4dc3c0cb164029849398bc42623523,
title = "Ensuring the Reliability of Your Model Checker:: Interval Iteration for Markov Decision Processes",
abstract = "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. ",
author = "Christel Baier and Joachim Klein and Linda Leuschner and David Parker",
year = "2017",
month = jul,
doi = "10.1007/978-3-319-63387-9_8",
language = "English",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "160--180",
editor = "Rupak Majumdar and Viktor Kun{\v c}ak",
booktitle = "Computer Aided Verification",
note = "Computer Aided Verification, 29th International Conference, CAV 2017 ; Conference date: 22-07-2017 Through 28-07-2017",

}

RIS

TY - GEN

T1 - Ensuring the Reliability of Your Model Checker:

T2 - Computer Aided Verification, 29th International Conference

AU - Baier, Christel

AU - Klein, Joachim

AU - Leuschner, Linda

AU - Parker, David

PY - 2017/7

Y1 - 2017/7

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-63387-9_8

DO - 10.1007/978-3-319-63387-9_8

M3 - Conference contribution

T3 - Lecture Notes in Computer Science

SP - 160

EP - 180

BT - Computer Aided Verification

A2 - Majumdar, Rupak

A2 - Kunčak, Viktor

PB - Springer

Y2 - 22 July 2017 through 28 July 2017

ER -