Incremental Verification of Parametric and Reconfigurable Markov Chains

Paul Gainer, Ernst Moritz Hahn, University Liverpool, Sven Schewe

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

5 Citations (Scopus)
137 Downloads (Pure)


The analysis of parametrised systems is a growing field in verification, but the analysis of parametrised probabilistic systems is still in its infancy. This is partly because it is much harder: while there are beautiful cut-off results for non-stochastic systems that allow to focus only on small instances, there is little hope that such approaches extend to the quantitative analysis of probabilistic systems, as the probabilities depend on the size of a system. The unicorn would be an automatic transformation of a parametrised system into a formula, which allows to plot, say, the likelihood to reach a goal or the expected costs to do so, against the parameters of a system. While such analysis exists for narrow classes of systems, such as waiting queues, we aim both lower—stepwise exploring the parameter space—and higher—considering general systems.

The novelty is to heavily exploit the similarity between instances of parametrised systems. When the parameter grows, the system for the smaller parameter is, broadly speaking, present in the larger system. We use this observation to guide the elegant state-elimination method for parametric Markov chains in such a way, that the model transformations will start with those parts of the system that are stable under increasing the parameter. We argue that this can lead to a very cheap iterative way to analyse parametric systems, show how this approach extends to reconfigurable systems, and demonstrate on two benchmarks that this approach scales.
Original languageEnglish
Title of host publicationQuantitative Evaluation of Systems - 15th International Conference, QEST 2018, Beijing, China, September 4-7, 2018: Proceedings
Number of pages17
Publication statusPublished - 2018

Publication series

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


Dive into the research topics of 'Incremental Verification of Parametric and Reconfigurable Markov Chains'. Together they form a unique fingerprint.

Cite this