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.
|Title of host publication||International Symposium on Automated Technology for Verification and Analysis, 2018|
|Number of pages||17|
|Publication status||Published - 30 Sep 2018|
|Name||Lecture notes in Computer Science|
Gainer, P., Hahn, E. M., & Schewe, S. (2018). Accelerated Model Checking of Parametric Markov Chains. In International Symposium on Automated Technology for Verification and Analysis, 2018 (pp. 300-316). (Lecture notes in Computer Science; Vol. 11138). https://doi.org/10.1007/978-3-030-01090-4_18