# 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.*