Incremental verification of parametric and reconfigurable markov chains

Paul Gainer*, Ernst Moritz Hahn, Sven Schewe

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

5 Citations (Scopus)


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
Subtitle of host publication15th International Conference, QEST 2018, Beijing, China, September 4-7, 2018, Proceedings
EditorsAndras Horvath, Annabelle McIver
Place of PublicationCham
Number of pages17
ISBN (Electronic)978-3-319-99154-2
ISBN (Print)978-3-319-99153-5
Publication statusPublished - 2018
Externally publishedYes
Event15th International Conference on Quantitative Evaluation of Systems, QEST 2018 - UCAS Campus, Beijing, China
Duration: 4 Sept 20187 Sept 2018
Conference number: 15

Publication series

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


Conference15th International Conference on Quantitative Evaluation of Systems, QEST 2018
Abbreviated titleQEST 2018
Internet address


  • Markov Chain Parameters (PMC)
  • State elimination
  • Incident transitions
  • Zeroconf protocol
  • Volatile areas


Dive into the research topics of 'Incremental verification of parametric and reconfigurable markov chains'. Together they form a unique fingerprint.

Cite this