Accelerated Model Checking of Parametric Markov Chains

Schewe, S ORCID: 0000-0002-9093-9518, Gainer, Paul and Hahn, Ernst Moritz (2018) Accelerated Model Checking of Parametric Markov Chains. In: International Symposium on Automated Technology for Verification and Analysis, 2018-10-7 - 2018-10-10, Los Angeles.

Text atva18.pdf - Author Accepted Manuscript Download (411kB)

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.

Item Type:	Conference or Workshop Item (Unspecified)
Depositing User:	Symplectic Admin
Date Deposited:	14 Jan 2019 16:05
Last Modified:	19 Jan 2023 01:30
DOI:	10.1007/978-3-030-01090-4_18
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3023863