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 proceedingChapterAcademicpeer-review

11 Citations (Scopus)


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 languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis
Subtitle of host publication16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings
EditorsShuvendu K. Lahiri, Chao Wang
Place of PublicationCham
ISBN (Electronic)978-3-030-01090-4
ISBN (Print)978-3-030-01089-8
Publication statusPublished - 2018
Externally publishedYes
Event16th International Symposium on Automated Technology for Verification and Analysis, ATVA 2018 - Los Angeles, United States
Duration: 7 Oct 201810 Oct 2018
Conference number: 16

Publication series

NameLecture Notes in Computer Science
ISSN (Print)1611-3349
ISSN (Electronic)1611-3349


Conference16th International Symposium on Automated Technology for Verification and Analysis, ATVA 2018
Abbreviated titleATVA
Country/TerritoryUnited States
CityLos Angeles


Dive into the research topics of 'Accelerated Model Checking of Parametric Markov Chains'. Together they form a unique fingerprint.

Cite this