  Markov chain analysis is a key technique in formal verification. A practical
obstacle is that all probabilities in Markov models need to be known. However,
system quantities such as failure rates or packet loss ratios, etc. are often
not -- or only partially -- known. This motivates considering parametric models
with transitions labeled with functions over parameters. Whereas traditional
Markov chain analysis relies on a single, fixed set of probabilities, analysing
parametric Markov models focuses on synthesising parameter values that
establish a given safety or performance specification $\varphi$. Examples are:
what component failure rates ensure the probability of a system breakdown to be
below 0.00000001?, or which failure rates maximise the performance, for
instance the throughput, of the system? This paper presents various analysis
algorithms for parametric discrete-time Markov chains and Markov decision
processes. We focus on three problems: (a) do all parameter values within a
given region satisfy $\varphi$?, (b) which regions satisfy $\varphi$ and which
ones do not?, and (c) an approximate version of (b) focusing on covering a
large fraction of all possible parameter values. We give a detailed account of
the various algorithms, present a software tool realising these techniques, and
report on an extensive experimental evaluation on benchmarks that span a wide
range of applications.
