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

4 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 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
PublisherSpringer
Pages300-316
ISBN (Electronic)978-3-030-01090-4
ISBN (Print)978-3-030-01089-8
DOIs
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
PublisherSpringer
Volume11138
ISSN (Print)1611-3349
ISSN (Electronic)1611-3349

Conference

Conference16th International Symposium on Automated Technology for Verification and Analysis, ATVA 2018
Abbreviated titleATVA
CountryUnited States
CityLos Angeles
Period7/10/1810/10/18

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

Cite this