Progress in Parameter Synthesis for Markov Models

A major practical obstacle in probabilistic verification is that all
probabilities (rates) in Markov models have to be fixed. However, at
early development stages, certain system quantities such as failure
rates, reaction speed, packet loss ratios, etc. are often not —- or at
best partially —- known. This motivates to consider parametric models
with transition probabilities specified as functions over parameters.

We consider parameter synthesis: Given a parametric Markov model, what
are the parameter values for which a given property exceeds a given
threshold? For example, what failure rates are tolerable ensuring that
the likelihood of a system breakdown is below 0,00000001?

We present an exact SMT-approach that significantly outperforms the
competitive approaches. Then we discuss a simple approximate technique
whose beauty is its applicability to various models such as Markov
chains, MDPs, and stochastic games. To conclude, we sketch the use of
geometric programming to treat various parameters and multi-objective
properties.