A Comparison of Time- and Reward-Bounded Probabilistic Model Checking Techniques

Ernst Moritz Hahn, Arnd Hartmanns

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

4 Citations (Scopus)
61 Downloads (Pure)

Abstract

In the design of probabilistic timed systems, requirements concerning behaviour that occurs within a given time or energy budget are of central importance. We observe that model-checking such requirements for probabilistic timed automata can be reduced to checking reward-bounded properties on Markov decision processes. This is traditionally implemented by unfolding the model according to the bound, or by solving a sequence of linear programs. Neither scales well to large models. Using value iteration in place of linear programming achieves scalability but accumulates approximation error. In this paper, we correct the value iteration-based scheme, present two new approaches based on scheduler enumeration and state elimination, and compare the practical performance and scalability of all techniques on a number of case studies from the literature. We show that state elimination can significantly reduce runtime for large models or high bounds.
Original languageEnglish
Title of host publicationProceedings of the Second International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016)
Place of PublicationCham
PublisherSpringer
Pages85-100
Number of pages16
ISBN (Print)978-3-319-47676-6
DOIs
Publication statusPublished - Nov 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume9984
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Model checking
Scalability
Linear programming
Statistical Models

Keywords

  • EWI-27541
  • METIS-320924
  • IR-103039

Cite this

Hahn, E. M., & Hartmanns, A. (2016). A Comparison of Time- and Reward-Bounded Probabilistic Model Checking Techniques. In Proceedings of the Second International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016) (pp. 85-100). (Lecture Notes in Computer Science; Vol. 9984). Cham: Springer. https://doi.org/10.1007/978-3-319-47677-3_6
Hahn, Ernst Moritz ; Hartmanns, Arnd. / A Comparison of Time- and Reward-Bounded Probabilistic Model Checking Techniques. Proceedings of the Second International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016). Cham : Springer, 2016. pp. 85-100 (Lecture Notes in Computer Science).
@inproceedings{4f5f29e9cf0a4bf2a5e48c7554cf8cbf,
title = "A Comparison of Time- and Reward-Bounded Probabilistic Model Checking Techniques",
abstract = "In the design of probabilistic timed systems, requirements concerning behaviour that occurs within a given time or energy budget are of central importance. We observe that model-checking such requirements for probabilistic timed automata can be reduced to checking reward-bounded properties on Markov decision processes. This is traditionally implemented by unfolding the model according to the bound, or by solving a sequence of linear programs. Neither scales well to large models. Using value iteration in place of linear programming achieves scalability but accumulates approximation error. In this paper, we correct the value iteration-based scheme, present two new approaches based on scheduler enumeration and state elimination, and compare the practical performance and scalability of all techniques on a number of case studies from the literature. We show that state elimination can significantly reduce runtime for large models or high bounds.",
keywords = "EWI-27541, METIS-320924, IR-103039",
author = "Hahn, {Ernst Moritz} and Arnd Hartmanns",
note = "eemcs-eprint-27541",
year = "2016",
month = "11",
doi = "10.1007/978-3-319-47677-3_6",
language = "English",
isbn = "978-3-319-47676-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "85--100",
booktitle = "Proceedings of the Second International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016)",

}

Hahn, EM & Hartmanns, A 2016, A Comparison of Time- and Reward-Bounded Probabilistic Model Checking Techniques. in Proceedings of the Second International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016). Lecture Notes in Computer Science, vol. 9984, Springer, Cham, pp. 85-100. https://doi.org/10.1007/978-3-319-47677-3_6

A Comparison of Time- and Reward-Bounded Probabilistic Model Checking Techniques. / Hahn, Ernst Moritz; Hartmanns, Arnd.

Proceedings of the Second International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016). Cham : Springer, 2016. p. 85-100 (Lecture Notes in Computer Science; Vol. 9984).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - A Comparison of Time- and Reward-Bounded Probabilistic Model Checking Techniques

AU - Hahn, Ernst Moritz

AU - Hartmanns, Arnd

N1 - eemcs-eprint-27541

PY - 2016/11

Y1 - 2016/11

N2 - In the design of probabilistic timed systems, requirements concerning behaviour that occurs within a given time or energy budget are of central importance. We observe that model-checking such requirements for probabilistic timed automata can be reduced to checking reward-bounded properties on Markov decision processes. This is traditionally implemented by unfolding the model according to the bound, or by solving a sequence of linear programs. Neither scales well to large models. Using value iteration in place of linear programming achieves scalability but accumulates approximation error. In this paper, we correct the value iteration-based scheme, present two new approaches based on scheduler enumeration and state elimination, and compare the practical performance and scalability of all techniques on a number of case studies from the literature. We show that state elimination can significantly reduce runtime for large models or high bounds.

AB - In the design of probabilistic timed systems, requirements concerning behaviour that occurs within a given time or energy budget are of central importance. We observe that model-checking such requirements for probabilistic timed automata can be reduced to checking reward-bounded properties on Markov decision processes. This is traditionally implemented by unfolding the model according to the bound, or by solving a sequence of linear programs. Neither scales well to large models. Using value iteration in place of linear programming achieves scalability but accumulates approximation error. In this paper, we correct the value iteration-based scheme, present two new approaches based on scheduler enumeration and state elimination, and compare the practical performance and scalability of all techniques on a number of case studies from the literature. We show that state elimination can significantly reduce runtime for large models or high bounds.

KW - EWI-27541

KW - METIS-320924

KW - IR-103039

U2 - 10.1007/978-3-319-47677-3_6

DO - 10.1007/978-3-319-47677-3_6

M3 - Conference contribution

SN - 978-3-319-47676-6

T3 - Lecture Notes in Computer Science

SP - 85

EP - 100

BT - Proceedings of the Second International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016)

PB - Springer

CY - Cham

ER -

Hahn EM, Hartmanns A. A Comparison of Time- and Reward-Bounded Probabilistic Model Checking Techniques. In Proceedings of the Second International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016). Cham: Springer. 2016. p. 85-100. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-47677-3_6