Résumé | Markov models comprise states with probabilistic transitions..
The analysis of these models is ubiquitous and studied in,
among others, reliability engineering, artificial intelligence, systems biology, and formal methods.
Naturally, their analysis crucially depends on the transition probabilities.
Often, these probabilities are approximations based on data or reflect configurable parts of a modelled system.
To represent the uncertainty about the probabilities, we study parametric Markov models,
in which the probabilities are symbolic expressions rather than concrete values.
More precisely, we consider parametric Markov decision processes (pMDPs) and parametric Markov chains (pMCs) as special case.
Substitution of the parameters yields classical, parameter-free Markov decision processes (MDPs) and Markov chains (MCs).
A pMDP thus induces uncountably many MDPs.
Each MDP may satisfy reachability and reward properties, such as the maximal probability that the system reaches an `offline' state is less than 0.01%.
Lifting these properties to pMDPs yields fundamental problems asking, e.g., Is there an induced MDP satisfying the property?
We give an overview over such problems on a conceptual level, discuss their complexity, and survey both older and recent methods. |