Parameter Synthesis for Markov Models
We consider variants of probabilistic model checking. Traditionally, model checking asks whether a given model fulfils a given specification. A model in this context describes possible system states, and the effect that an event has on the state space. A typical specification is: „A dangerous state cannot be reached“
Probabilistic model checking considers models which contain probabilistic uncertainties, where, e.g., the outcome of some action or event is given by a distribution over the state space. Typical specifications now are: „The probability of reaching a bad state is below 1%“ or „The expected time until reaching some goal is less than an hour.“
The probabilities in probabilistic models can be categorised into two groups:
Often, the distributions in these models are approximations of the actual system behaviour, typically obtained by a series of experiments: the (transition) probabilities are then uncontrollable and uncertain.
Or, the randomisation is an integral part of the system design, as common in randomised algorithms: the probabilities are then controllable.
For both types of models, we are interested in the effect of changing parameters. Thus, we answer questions like “Do transition probabilities exist such that the probability of reaching a bad state is below 1%”, “Is the probability of reaching a bad state below 1% for all transition probabilities”, etc.