Accelerated Model Checking of Parametric Markov Chains

Paul Gainer, Ernst Moritz Hahn, Sven Schewe

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

15 Citations (Scopus)
281 Downloads (Pure)


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 publicationInternational Symposium on Automated Technology for Verification and Analysis, 2018
Number of pages17
ISBN (Electronic)978-3-030-01090-4
Publication statusPublished - 30 Sept 2018

Publication series

NameLecture notes in Computer Science
ISSN (Print)0302-9743


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

Cite this