Accelerated Model Checking of Parametric Markov Chains

Paul Gainer; Ernst Moritz  Hahn; Sven Schewe

doi:10.1007/978-3-030-01090-4_18

Accelerated Model Checking of Parametric Markov Chains

Paul Gainer, Ernst Moritz Hahn^*, Sven Schewe

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

11 Citations (Scopus)

Abstract

Parametric Markov chains occur quite naturally in various applications: they can be used for a conservative analysis of probabilistic systems (no matter how the parameter is chosen, the system works to specification); they can be used to find optimal settings for a parameter; they can be used to visualise the influence of system parameters; and they can be used to make it easy to adjust the analysis for the case that parameters change. Unfortunately, these advancements come at a cost: parametric model checking is—or rather was—often slow. To make the analysis of parametric Markov models scale, we need three ingredients: clever algorithms, the right data structure, and good engineering. Clever algorithms are often the main (or sole) selling point; and we face the trouble that this paper focuses on – the latter ingredients to efficient model checking. Consequently, our easiest claim to fame is in the speed-up we have often realised when comparing to the state of the art.

Original language	English
Title of host publication	Automated Technology for Verification and Analysis
Subtitle of host publication	16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings
Editors	Shuvendu K. Lahiri, Chao Wang
Place of Publication	Cham
Publisher	Springer
Pages	300-316
ISBN (Electronic)	978-3-030-01090-4
ISBN (Print)	978-3-030-01089-8
DOIs	https://doi.org/10.1007/978-3-030-01090-4_18
Publication status	Published - 2018
Externally published	Yes
Event	16th International Symposium on Automated Technology for Verification and Analysis, ATVA 2018 - Los Angeles, United States Duration: 7 Oct 2018 → 10 Oct 2018 Conference number: 16

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	11138
ISSN (Print)	1611-3349
ISSN (Electronic)	1611-3349

Conference

Conference	16th International Symposium on Automated Technology for Verification and Analysis, ATVA 2018
Abbreviated title	ATVA
Country/Territory	United States
City	Los Angeles
Period	7/10/18 → 10/10/18

Access to Document

10.1007/978-3-030-01090-4_18

Cite this

Gainer, P., Hahn, E. M., & Schewe, S. (2018). Accelerated Model Checking of Parametric Markov Chains. In S. K. Lahiri, & C. Wang (Eds.), Automated Technology for Verification and Analysis: 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings (pp. 300-316). (Lecture Notes in Computer Science; Vol. 11138). Springer. https://doi.org/10.1007/978-3-030-01090-4_18

@inbook{9c91c97c3fb540a4902bc3f6634f8000,

title = "Accelerated Model Checking of Parametric Markov Chains",

abstract = "Parametric Markov chains occur quite naturally in various applications: they can be used for a conservative analysis of probabilistic systems (no matter how the parameter is chosen, the system works to specification); they can be used to find optimal settings for a parameter; they can be used to visualise the influence of system parameters; and they can be used to make it easy to adjust the analysis for the case that parameters change. Unfortunately, these advancements come at a cost: parametric model checking is—or rather was—often slow. To make the analysis of parametric Markov models scale, we need three ingredients: clever algorithms, the right data structure, and good engineering. Clever algorithms are often the main (or sole) selling point; and we face the trouble that this paper focuses on – the latter ingredients to efficient model checking. Consequently, our easiest claim to fame is in the speed-up we have often realised when comparing to the state of the art.",

author = "Paul Gainer and Hahn, {Ernst Moritz} and Sven Schewe",

year = "2018",

doi = "10.1007/978-3-030-01090-4_18",

language = "English",

isbn = "978-3-030-01089-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "300--316",

editor = "Lahiri, {Shuvendu K.} and Chao Wang",

booktitle = "Automated Technology for Verification and Analysis",

note = "16th International Symposium on Automated Technology for Verification and Analysis, ATVA 2018, ATVA ; Conference date: 07-10-2018 Through 10-10-2018",

}

Gainer, P, Hahn, EM & Schewe, S 2018, Accelerated Model Checking of Parametric Markov Chains. in SK Lahiri & C Wang (eds), Automated Technology for Verification and Analysis: 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11138, Springer, Cham, pp. 300-316, 16th International Symposium on Automated Technology for Verification and Analysis, ATVA 2018, Los Angeles, California, United States, 7/10/18. https://doi.org/10.1007/978-3-030-01090-4_18

Accelerated Model Checking of Parametric Markov Chains. / Gainer, Paul; Hahn, Ernst Moritz ; Schewe, Sven.

Automated Technology for Verification and Analysis: 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings. ed. / Shuvendu K. Lahiri; Chao Wang. Cham : Springer, 2018. p. 300-316 (Lecture Notes in Computer Science; Vol. 11138).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

TY - CHAP

T1 - Accelerated Model Checking of Parametric Markov Chains

AU - Gainer, Paul

AU - Hahn, Ernst Moritz

AU - Schewe, Sven

N1 - Conference code: 16

PY - 2018

Y1 - 2018

N2 - Parametric Markov chains occur quite naturally in various applications: they can be used for a conservative analysis of probabilistic systems (no matter how the parameter is chosen, the system works to specification); they can be used to find optimal settings for a parameter; they can be used to visualise the influence of system parameters; and they can be used to make it easy to adjust the analysis for the case that parameters change. Unfortunately, these advancements come at a cost: parametric model checking is—or rather was—often slow. To make the analysis of parametric Markov models scale, we need three ingredients: clever algorithms, the right data structure, and good engineering. Clever algorithms are often the main (or sole) selling point; and we face the trouble that this paper focuses on – the latter ingredients to efficient model checking. Consequently, our easiest claim to fame is in the speed-up we have often realised when comparing to the state of the art.

AB - Parametric Markov chains occur quite naturally in various applications: they can be used for a conservative analysis of probabilistic systems (no matter how the parameter is chosen, the system works to specification); they can be used to find optimal settings for a parameter; they can be used to visualise the influence of system parameters; and they can be used to make it easy to adjust the analysis for the case that parameters change. Unfortunately, these advancements come at a cost: parametric model checking is—or rather was—often slow. To make the analysis of parametric Markov models scale, we need three ingredients: clever algorithms, the right data structure, and good engineering. Clever algorithms are often the main (or sole) selling point; and we face the trouble that this paper focuses on – the latter ingredients to efficient model checking. Consequently, our easiest claim to fame is in the speed-up we have often realised when comparing to the state of the art.

U2 - 10.1007/978-3-030-01090-4_18

DO - 10.1007/978-3-030-01090-4_18

M3 - Chapter

SN - 978-3-030-01089-8

T3 - Lecture Notes in Computer Science

SP - 300

EP - 316

BT - Automated Technology for Verification and Analysis

A2 - Lahiri, Shuvendu K.

A2 - Wang, Chao

PB - Springer

CY - Cham

T2 - 16th International Symposium on Automated Technology for Verification and Analysis, ATVA 2018

Y2 - 7 October 2018 through 10 October 2018

ER -

Accelerated Model Checking of Parametric Markov Chains

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this