Parameter synthesis

Analysis of parametric Markov models

Probabilistic model checking commonly assumes that the transition probabilities are precisely known. This assumption, however, is often impractical in reality. Parametric Markov models allow to represent these uncertain probabilities through parameters. Analysis of parametric Markov models then aims to answer questions such as “for which parameter values does the specification hold?” or synthesize parameter values which lead to optimal performance.

We developed analysis techniques for parametric discrete-time Markov chains (Jansen et al., 2014) and provided tool support in Storm or the dedicated Prophesy tool (Dehnert et al., 2015). We also developed an analysis approach for continuous-time Markov chains with transition rates sampled from a prior distribution. The approach employs sampling-based techniques and yields the most likely behavior of the model – with a given confidence (Badings et al., 2022).


We applied parameter synthesis to find the optimal bias for randomized distributed algorithms (Volk et al., 2022).



  1. DC
    Matthias VolkBorzoo BonakdarpourJoost-Pieter Katoen, and Saba Aflaki
    Distributed Comput., 2022


  1. CAV
    Christian Dehnert, Sebastian JungesNils Jansen, Florian Corzilius, Matthias Volk, Harold Bruintjes, Joost-Pieter Katoen, and Erika Ábrahám
    In CAV (1), 2015


  1. QEST
    Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika ÁbrahámJoost-Pieter Katoen, and Bernd Becker
    In QEST, 2014