Accelerated Model Checking of Parametric Markov Chains

Paul Gainer, Ernst Moritz Hahn, Sven Schewe

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

4 Citations (Scopus)
180 Downloads (Pure)

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

Publication series

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

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

Cite this