11institutetext:  Radboud University, Nijmegen, The Netherlands
22institutetext: RWTH Aachen University, Aachen, Germany

# Parameter Synthesis in Markov Models:
A Gentle Survey††thanks: This work has been supported by the DFG RTG 2236
“UnRAVeL” and the ERC Advanced Grant 787914 “FRAPPANT”.

Nils Jansen 11 Sebastian Junges and Joost-Pieter Katoen 1122

###### Abstract

This paper surveys the analysis of parametric Markov models whose transitions
are labelled with functions over a finite set of parameters. These models are
symbolic representations of uncountable many concrete probabilistic models,
each obtained by instantiating the parameters. We consider various analysis
problems for a given logical specification $\varphi$: do all parameter
instantiations within a given region of parameter values satisfy $\varphi$?,
which instantiations satisfy $\varphi$ and which ones do not?, and how can all
such instantiations be characterised, either exactly or approximately? We
address theoretical complexity results and describe the main ideas underlying
state-of-the-art algorithms that established an impressive leap over the last
decade enabling the fully automated analysis of models with millions of states
and thousands of parameters.

##  1 Introduction

Markov models are ubiquitous. Markov chains (MCs) are central in performance
and dependability analysis, whereas Markov decision processes (MDPs) are key
in stochastic decision making and planning in AI. A standard assumption in
these models is that all probabilities are precisely known. This assumption is
often too severe. System quantities such as component fault rates, molecule
reaction rates, packet loss ratios, etc. are often not, or at best partially,
known.

Figure 1: For which gate failure rates is the circuit reliable?

##### A motivating example.

In early stages of reliable system design, the concrete failure rate of
components [28] is deliberately left unspecified. Let us illustrate this by
considering a multiplexed NAND integrated circuit. As such circuits are built
at ever smaller scale, they are prone to defects and/or to exhibit transient
failures. The analysis of a parametric Markov chain model of the NAND circuit
[44] can provide insights into the effect of failure probabilities of the
gates on the overall circuit’s reliability. The unknown random gate failure
rates are the model’s parameters. Questions of interest are e.g., for which
gate failure rates are at least 70% of the NAND outputs correct, or which
failure rates minimise the circuit’s reliability? More advanced objectives are
to determine either exactly or approximately _all_ possible failure rates such
that the NAND’s failure probability is below $\nicefrac{{3}}{{10}}$, or even
to provide a closed-form formula of how the circuit’s reliability depends on
the vulnerability of its gates. Fig. 1, for instance, plots exact synthesis
results (obtained in a few minutes) for two gates with unknown failure rate
($x$\- and $y$-axis) indicating all gate’s failure rates leading to circuit
failure probabilities ($z$-axis) above (red) and below (green) the threshold
$\nicefrac{{3}}{{10}}$.

##### Aims of this paper.

Our aim is to provide insight in the underlying algorithmic techniques and the
complexity to answer the above questions of interest. We do so by surveying
the automated analysis of parametric Markov models. For the sake of
simplicity, we consider _parametric Markov chains (pMCs)_ and do not consider
parametric versions of MDPs. Yet, various of the presented techniques are also
applicable to non-deterministic models. Parametric MCs are classical discrete-
time Markov chains where the transition probabilities are specified by
polynomials over real-valued parameters, e.g., $x$, $1{-}x$, and $1{-}x{\cdot
y}{+}z$. Intervals over parameters are simple instances imposing constant
lower and upper bounds on each parameter [58, 38]. The setting here is more
liberal as it includes the possibility to express parameter dependencies: a
parameter can occur at several transitions. This often leads to solving trade-
offs: for some states it may beneficial to have a small value of parameter
$x$, whereas for other states a large value of $x$ is better, e.g., to
increase the probability to reach a certain target state.

##### Parameter synthesis problems.

We consider various problems for parametric MCs and a given logical
specification $\varphi$: (1) do all parameter instantiations, within a given
region of parameter values, satisfy $\varphi$?, (2) which instantiations
satisfy $\varphi$ and which ones do not?, and (3) how can all such
instantiations be characterised, either exactly or approximately? These
questions are intrinsically hard: parameters can take uncountable many
different values and the parameters may depend on each other. We address
theoretical complexity results and describe the main ideas underlying state-
of-the-art algorithms for (1) through (3). For the sake of simplicity, we
focus on specifications $\varphi$ that impose thresholds on infinite-horizon
reachability probabilities; e.g., can a bad state be reached with a
probability at most 10-6? The presented algorithms can however also be
generalised in a straightforward manner to total expected reward objectives
such as: is the expected cost to reach a goal state at most 103? This survey
aims to give an insight into the main advances during the last decade. Whereas
initial algorithms could only handle a handful of parameters111And this was
viewed by quite some scepticism, e.g., our initial paper on this topic
received reviews saying “this is a fun problem that is unlikely to ever result
in practical advancements.”, these advancements enable _the fully automated
analysis of models with millions of states and thousands of parameters_.

##### POMDP controller synthesis.

Parametric MCs can be seen as Markov chains with partial information about the
transition probabilities. Indeed, these transition probabilities are solutions
of functions over the parameters. As the choice of the parameter values is
assumed to be fully non-deterministic (these values are e.g., not subject to a
probability distribution), pMCs can be seen as a kind of MDP with partial
information. This raises the question whether there is a relation to the well-
known model of partially-observable MDPs (POMDPs) [57, 71, 75]. POMDPs are a
prominent model in sequential decision-making under uncertainty: decisions
have to be made under partial knowledge about the environment. Intuitively,
POMDP policies (aka: controllers) have to make optimal decisions based on
partial information about the visited states. Indeed, there exists a direct
link between parameter synthesis for pMCs and controller synthesis for POMDPs.
In fact, finding a finite-memory policy that guarantees the satisfaction of a
reachability property $\varphi$ in a POMDP is equivalent to feasibility — find
a parameter instantiation satisfying $\varphi$ — in a corresponding pMC.

##### Highlights.

Section 4 shows that the decision problem of feasibility, does there exist a
parameter instantiation such that specification $\varphi$ is satisfied, is
ETR-complete. In particular, the fact that ETR-satisfiability problems can be
encoded as reachability problems in pMCs is of interest. Section 5.4 describes
how convex optimisation can be used to solve feasibility approximatively and
how a tight integration with model checking improves this further. Section 5.2
describes an abstraction-based approach that reduces checking whether a region
of parameter instantiations satisfies $\varphi$ on a pMC to a parameter-less
model checking problem on an MDP. Section 6 details the connection between
feasibility in pMCs to POMDP controller synthesis. This link closes a
complexity gap in POMDP controller synthesis, and enables using parameter
synthesis algorithms such as the integrated model checking–convex optimisation
for POMDP controller synthesis. Almost all sections include indications about
the kind of synthesis problems (in terms of model size, number of parameters,
and precision) that can be solved using current algorithms and software tools.

##  2 Parametric Markov Chains

Let $X$ be a set of $n$ real-valued parameters (or variables)
$x_{1},\ldots,x_{n}$. The parameters $x_{i}$ should be considered as symbols.
Their values are defined by a parameter instantiation, i.e., a function
$v\colon X\to\mathbb{R}$. The set $V\subseteq\mathbb{R}^{n}$ of all parameter
values is called the parameter space. A set $R\subseteq V$ of instantiations
is a _region_.

Let $\mathbb{Q}[X]$ denote the set of multivariate polynomials over $X$ with
rational coefficients. A polynomial $f\in\mathbb{Q}[X]$ can be interpreted as
a function $f\colon\mathbb{R}^{n}\to\mathbb{R}$ where $f(v)$ is obtained by
replacing each occurrence of $x_{i}$ in $f$ by $v(x_{i})$; e.g., for
$f=2x_{1}{\cdot}x_{2}+x_{1}^{2}$ with $v(x_{1})=2$ and $v(x_{2})=3$, we have
$f(v)=16$. To make clear where substitution occurs, we write $f[v]$ instead of
$f(v)$ from now on.

###### Definition 1

A pMC $\mathcal{D}$ is a tuple $(S,s_{\mathit{I}},X,\mathcal{P})$ with a
finite set $S$ of _states_ , an _initial state_ $s_{\mathit{I}}\in S$, a
finite set $X$ of real-valued variables _(parameters)_ and a _transition
function_ $\mathcal{P}\colon S\times S\to\mathbb{Q}[X]$.

$s_{0}$$s_{1}$$s_{2}$$s_{3}$$s_{4}$$s_{5}$$s_{6}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$

(a) fair coins

$s_{0}$$s_{1}$$s_{2}$$s_{3}$$s_{4}$$s_{5}$$s_{6}$$\nicefrac{{2}}{{5}}$$\nicefrac{{3}}{{5}}$$\nicefrac{{7}}{{10}}$$\nicefrac{{3}}{{10}}$$\nicefrac{{2}}{{5}}$$\nicefrac{{3}}{{5}}$$\nicefrac{{3}}{{5}}$$\nicefrac{{2}}{{5}}$$\nicefrac{{7}}{{10}}$$\nicefrac{{3}}{{10}}$$\nicefrac{{2}}{{5}}$$\nicefrac{{3}}{{5}}$$\nicefrac{{3}}{{5}}$$\nicefrac{{2}}{{5}}$

(b) biased coins

$s_{0}$$s_{1}$$s_{2}$$s_{3}$$s_{4}$$s_{5}$$s_{6}$$x$$1-x$$y$$1-y$$x$$1-x$$1-x$$x$$y$$1-y$$x$$1-x$$1-x$$x$

(c) coins with unknown bias

Figure 2: Three variations of the Knuth-Yao die

The parametric transition probability of going from state $s$ to $t$ is given
by $\mathcal{P}(s,t)$. Intuitively, instead of a concrete probability, a
transition is equipped with a polynomial over the parameters $X$, e.g.,
$\mathcal{P}(s,t)=x^{2}{+}2{\cdot}y$. A pMC with $X=\varnothing$ is a
classical Markov chain (MC). Applying an instantiation $v$ to a pMC
$\mathcal{D}$ yields MC $\mathcal{D}[v]$ by replacing each transition
$\mathcal{P}(s,t)=f\in\mathbb{Q}[X]$ in $\mathcal{D}$ by $f[v]$. In general, a
pMC defines an uncountable infinite family of MCs where each family member is
obtained by a parameter instantiation. We assume every instantiation $v$ of
$\mathcal{D}$ to yield well-defined MCs, i.e., $\mathcal{P}(s,\cdot)[v]$ is a
probability distribution over the set $S$ of states; e.g., values $v(x)$ and
$v(y)$ for $\mathcal{P}(s,t)=x^{2}{+}2y$ should be such that $0\leqslant
v(x)^{2}{+}2{\cdot}v(y)\leqslant 1$. For a detailed treatment we refer to [51,
50]. An instantiation $v$ is _graph-preserving_ (for $\mathcal{D}$) if the
topology of $\mathcal{D}$ is preserved, i. e., $\mathcal{P}(s,s^{\prime})\neq
0$ implies $\mathcal{P}(s,s^{\prime})[v]\neq 0$ for all $s,s^{\prime}\in S$. A
region $R$ is graph-preserving if every $v\in R$ is graph preserving.

###### Example 1

Fig. 2(a) depicts an MC with 13 states representing the Knuth-Yao algorithm
[56] that mimics a six-sided die by repeatedly flipping a fair coin. Fig. 2(b)
shows a version that uses two coins (in the white and gray states
respectively) with different but fixed biases. Fig. 2(c) provides a parametric
version where the two coins have an unknown bias. The parameters $x$ and $y$
represent the probability to throw heads in the gray and white states,
respectively. The parameter space is $\\{(x,y)\mid 0<x,y<1\\}$. The
instantiation $v$ with $v(x)=\nicefrac{{2}}{{5}}$ and
$v(y)=\nicefrac{{7}}{{10}}$ results in the MC in Fig. 2(b). The region of
“almost fair” coins $x$ and $y$, say the coins that are fair up to a possible
deviation of $\nicefrac{{1}}{{10}}$, is given by $\\{v\colon
X\to\mathbb{R}\mid\nicefrac{{9}}{{20}}\leqslant
v(x),v(y)\leqslant\nicefrac{{11}}{{20}}\\}$.

##  3 Parameter Synthesis Problems

Figure 3: Approximate partitioning to reach  with probability
$<\nicefrac{{3}}{{20}}$

A typical specification $\varphi$ requires to eventually reach a set of target
states in pMC $\mathcal{D}$ with at least (or at most) a certain probability.
A non-parametric MC $D$ satisfies $\varphi$, denoted $D\models\varphi$, if the
reachability probability of the target states meets this threshold for its
fixed transition probabilities. In the presence of parameters, the validity of
$\varphi$ is considered with respect to a given region $R$ of admissible
parameter values. Although this survey focuses on reachability probabilities
this is not a severe restriction. For instance, reachability probabilities
suffice to determine the probability to satisfy an $\omega$-regular
specification. Such specifications contain LTL formulas and coincide with
languages accepted by automata on infinite words such as non-deterministic
Büchi automata. The probability to satisfy $\omega$-regular specification
$\varphi$ in a non-parametric MC $D$ equals the reachability probability of
certain222The ones that are accepting according to the type (e.g., Muller,
Rabin) of deterministic automaton to encode $\varphi$. bottom strongly
connected components [80] in the synchronous product of $D$ with a
deterministic automaton on infinite words corresponding to $\varphi$. Similar
holds for the parametric setting. Alternative specifications involve rewards
(where $\mathcal{D}$ may have parametric rewards), bounded (aka: finite-
horizon) reachability, etc.

Let pMC $\mathcal{D}$ over $X=\\{x_{1},\ldots,x_{n}\\}$, specification
$\varphi$, and region $R\subseteq\mathbb{R}^{n}$. Let $v\in R$ stand for
instantiation $v\colon X\to\mathbb{R}$ with $v(x_{i})\in R{\upharpoonright}i$
for all $i$, and let:

$\mathcal{D},R\models\varphi\quad\text{iff}\quad\left(\forall v\in
R.\,\mathcal{D}[v]\models\varphi\right).$

We consider the following parameter synthesis problems:

  * •

The _feasibility problem_ is to check whether: $\exists v\in
R.\,\mathcal{D}[v]\models\varphi.$ Feasibility for $\varphi$ in $R$ is
equivalent to not $\left(\mathcal{D},R\models\neg\varphi\right)$.

  * •

The _optimal_ feasibility problem is to find an instantiation $v\in R$ that
maximises (or dually minimises) the probability to satisfy $\varphi$.

  * •

The _region verification problem_ is to check whether:

$\underbrace{\mathcal{D},R\models\varphi}_{R\text{ is
accepting}}\quad\text{or}\quad\underbrace{\mathcal{D},R\models\neg\varphi}_{R\text{
is rejecting}}\quad\text{or}\quad\underbrace{\mathcal{D},R\not\models\varphi\
\land\ \mathcal{D},R\not\models\neg\varphi}_{R\text{ is inconclusive}}.$

  * •

The _exact partitioning problem_ is to partition (measurable) $R$ into $R_{+}$
and $R_{-}$ such that:

$R_{+}=\\{\,v\in R\mid\mathcal{D}[v]\models\varphi\,\\}\quad\text{and}\quad
R_{-}=\\{\,v\in R\mid\mathcal{D}[v]\models\neg\varphi\,\\}.$

Instead of checking whether a region $R$ is accepting or rejecting, the exact
partitioning problem aims to find the largest subset of $R$ that is accepting
(or, dually, rejecting). As finding an exact partitioning is hard, often a
relaxed version is considered.

  * •

The _approximate partitioning problem_ is to partition (measurable) $R$ into
$R_{+}$, $R_{-}$, and $R_{?}$ such that for some given
$0\leqslant\eta\leqslant 1$:

$R_{+}\subseteq\\{\,v\in
R\mid\mathcal{D}[v]\models\varphi\,\\}\quad\text{and}\quad
R_{-}\subseteq\\{\,v\in R\mid\mathcal{D}[v]\models\neg\varphi\,\\},$

and $R_{?}=R\setminus(R_{+}\,\cup\,R_{-})$ with
$||R_{?}||\leqslant(1{-}\eta)\cdot||R||$ where $||\cdot||$ denotes the volume
of $R$. Here, $R_{?}$ is the fragment of $R$ that is inconclusive for
$\varphi$. It is required that this fragment occupies at most a factor
$1{-}\eta$ of the volume of $R$. Stated differently, the accepting and
rejecting region cover at least a factor $\eta$ of the region. Exact
partitioning is obtained if $\eta=1$.

###### Example 2

Consider the parametric die from Fig. 2(c) and let $\varphi$ be the
specification that the probability to reach state  is at least
$\nicefrac{{3}}{{20}}$. There exists a feasible solution, e.g.,
$x=y=\nicefrac{{1}}{{2}}$. Let region $R$ be all valuations with
$\nicefrac{{1}}{{10}}\leqslant v(x)\leqslant\nicefrac{{9}}{{10}}$ and
$\nicefrac{{3}}{{4}}\leqslant v(y)\leqslant\nicefrac{{5}}{{6}}$. It follows
that $R$ is accepting for $\neg\varphi$ (and thus rejecting $\varphi$) as for
all $v\in R$ the probability to reach  is at most $\nicefrac{{3}}{{20}}$. The
function:

$f(x,y)=\frac{x\cdot(1-y)\cdot(1-x)}{1-x\cdot y}$ (1)

describes the probability to reach . For $\neg\varphi$, $R_{+}=\\{v\mid
f[v]<\nicefrac{{3}}{{20}}\\}$ and $R_{-}=R\setminus R_{+}.$ Fig. 3 shows an
approximation (for $\eta=0.95$) of the function $f$ for $\neg\varphi$. The set
of rectangular accepting (green) regions indicate $R_{+}$ for $\neg\varphi$,
whereas the red (hatched) area indicates $R_{-}$. The white area indicates
$R_{?}$.

The synthesis problems are complex as — in contrast to interval MCs [58] —
parameters may depend on each other and may occur at several transitions in a
pMC. These dependencies lead to trade-offs: increasing a parameter value may
raise a reachability probability in one state but lower such probability in
another state. The next section addresses the theoretical complexity of the
feasibility problem.

##  4 Complexity of the Feasibility Problem

The ETR-SAT (Existential Theory of the Reals) decision problem consists of
deciding whether a given existentially quantified formula $\exists
x_{1}\ldots\exists x_{n}.\,F(x_{1},\ldots,x_{n})$ holds, where $F$ is a
Boolean combination of polynomial inequalities over the real-valued parameters
$x_{1}$ through $x_{n}$.333In SAT modulo theories, ETR is referred to as the
quantifier-free fragment of non-linear real arithmetic (QFNRA, for short). The
complexity class ETR contains all decision problems for which a polynomial
many-to-one reduction to the ETR-SAT decision problem exists. The class ETR
contains NP and is contained in PSPACE [17]. Given that the Boolean structure
of an ETR formula can be encoded into a polynomial, solving an ETR-SAT problem
is equally hard as determining whether a polynomial over $x_{1}$ through
$x_{n}$ has a real root.

Figure 4: A sample pMC for reachability probabilities

##### Encoding feasibility as ETR-SAT.

The following example illustrates that the feasibility problem can be reduced
to the ETR-SAT problem.

###### Example 3

Consider the pMC $\mathcal{D}$ in Fig. 4 with region $R=\\{v\mid
0<v(x),v(y)<1\\}$ and target state $s_{3}$. There exists a parameter
instantiation such that the specification $\varphi$ holds, i.e., $s_{3}$ is
reached with probability at least $\nicefrac{{3}}{{4}}$, whenever the
following ETR-formula holds:

$\begin{array}[]{l}\exists p_{0},\ldots,p_{3},x,y.\
\underbrace{0<x<1\,\land\,0<y<1}_{\footnotesize\mbox{region
}R}\,\land\,\underbrace{p_{1}\geqslant\nicefrac{{3}}{{4}}}_{\mbox{\footnotesize
spec. }\varphi}\\\\[4.30554pt] \phantom{\exists p_{0},\ldots,p_{3},x,y.}\
\wedge\ p_{3}=1\ \wedge\ p_{0}=0\\\\[4.30554pt] \phantom{\exists
p_{0},\ldots,p_{3},x,y.}\ \wedge\
p_{1}=x{\cdot}p_{2}+\underbrace{(1{-}x){\cdot}p_{0}}_{=0}\ \wedge\
p_{2}=y{\cdot}p_{1}+\underbrace{(1{-}y){\cdot}p_{3}}_{=1{-}y}.\end{array}$

A variable $p_{i}$ is introduced for each state $s_{i}$ in $\mathcal{D}$ that
intuitively represents the probability to eventually reach state $s_{3}$ from
$s_{i}$. Variables $x$ and $y$ represent the equally named parameters in
$\mathcal{D}$. The first line encodes the region $R$ and that $\varphi$ has to
hold for state $s_{1}$. The second line encodes that $s_{3}$ reaches itself
almost surely, and that $s_{3}$ can almost surely not be reached from $s_{0}$.
The equations in the last line express the recursive equations for
reachability probabilities. They conform to the form:

$\displaystyle p_{s}\ =\ \sum_{s^{\prime}\in
S_{>0}}\mathcal{P}(s,s^{\prime})\cdot p_{s^{\prime}}\quad\text{for all }s\in
S_{>0}\setminus G$ (2)

where $S_{>0}=\\{s_{1},s_{2},s_{3}\\}$ is the set of states that can reach a
state in the set of target states $G=\\{s_{3}\\}$. The size of the ETR-formula
is linear in the size of $\mathcal{D}$. The set $S_{>0}$ can be computed by
efficient graph analysis methods.

##### Encoding ETR-SAT as feasibility.

Interestingly, this reduction also works (under mild conditions) in the
reverse direction. We illustrate by example how to obtain an acyclic pMC
$\mathcal{D}_{F}$ from a given ETR-formula $F$ such that a target state can be
reached with probability at least $\lambda$ in $\mathcal{D}_{F}$ for some
variable instantiation $v$ if $F$ holds for $v$. This reduction relies on
important observations in [26]. The size of $\mathcal{D}_{F}$ is polynomial in
the degree of $F$, the number of terms in $F$, and the maximal number of bits
to encode the threshold $\lambda$ and $F$’s coefficients.

$\nicefrac{{2}}{{8}}$$\nicefrac{{2}}{{8}}$$\nicefrac{{2}}{{8}}$$\nicefrac{{1}}{{8}}$$1-x$$x$$y$$1-x$$y$$1-y$$y$
Figure 5: Sample construction for ETR-hardness for feasibility checking

###### Example 4

Consider the ETR-formula $F=\exists x,y.\,{-}2{\cdot}x^{2}{\cdot}y+y\geqslant
5$. We adapt this formula so as to remove the negative coefficients.
Simplification yields:

$2\cdot(1{-}x){\cdot}x{\cdot}y+2{\cdot}(1{-}x){\cdot}y+2{\cdot}(1{-}y)+y-2\
\geqslant\ 5.$

By adding $2$ and dividing by $8$, the coefficients describe a probability
distribution:

$\nicefrac{{2}}{{8}}{\cdot}(1{-}x){\cdot}x{\cdot}y+\nicefrac{{2}}{{8}}{\cdot}(1{-}x){\cdot}y+\nicefrac{{2}}{{8}}{\cdot}(1{-}y)+\nicefrac{{1}}{{8}}{\cdot}y\
\geqslant\ \nicefrac{{7}}{{8}}.$

The left-hand side of this inequation induces the pMC in Fig. 5, where the
missing transitions all lead to a sink state (omitted in the figure). The
probability to reach a target state is at least $\nicefrac{{7}}{{8}}$ if the
ETR-formula $F$ holds.

###### Theorem 4.1

[53] The feasibility problem for pMCs is ETR-complete.

A few remarks are in order. The reduction already applies to very simple
classes of pMCs, e.g., acyclic ones, and pMCs that only contain expressions
such as $x$ and $1{-}x$ on the transitions. Our next remark concerns the
complexity of related feasibility problems. The above results apply to
reachability objectives with non-strict conditions (i.e., either $\leqslant$
or $\geqslant$) on the probability thresholds. For strict conditions, the
feasibility problem is NP-hard. The feasibility problem for qualitative
reachability, i.e., thresholds 0 or 1, is NP-complete for most cases and in P
for specific cases such as graph-preserving instantiations. Our third remark
concerns pMCs with non-deterministic choices. The complexity class ETR is also
relevant for synthesis problems on parametric MDPs; e.g., the feasibility
problem “does there exist a parameter valuation such that for some (or,
dually, for all possible) resolution(s) of the non-determinism a reachability
probability meets a non-strict threshold” is ETR-complete too. Full details
can be found in [53]. As a fourth remark, we point out that the above result
holds for the setting with arbitrarily many parameters. If the number of
parameters is fixed, the feasibility problem for pMCs can be solved in
polynomial time [48, 7]. The complexity of the fixed parameter case for
parametric MDPs is still open. Finally, we note that the above result
indicates that solving the feasibility problem is difficult in general. This
motivates the search for heuristics and approximate techniques; such
techniques are discussed in Section 5.4.

##  5 Algorithms

This section describes the main underlying principles of algorithmic
approaches to tackle the aforementioned synthesis problems: exact and
approximate parameter space partitioning, region verification, and (optimal)
feasibility checking.

###  5.1 Exact Partitioning

Exact partitioning amounts to computing the rational function $f$ as e.g.,
given in equation (1). This function is commonly referred to as the _solution_
function (for the reachability objective “eventually ”). Computing a closed-
form solution function has been one of the first problems considered for pMCs
[32] and has been subject to several practical efficiency improvements, see
e.g., [40, 49, 36, 48, 7, 26, 35]. Solution functions map parameter values
onto reachability probabilities. For pMCs with polynomial transition functions
as in this survey, solution functions are lower semi-continuous; for acyclic
pMCs they are continuous.

##### Complexity.

The functions can be obtained by successively eliminating the state variables
from the characteristic equation system, e.g., the equations shown in Example
3. This procedure is in fact a Gaussian elimination procedure on the
parametric transition probability function. Phrased differently, one solves a
linear equation system with rational functions as coefficients.

###### Example 5

Consider again the pMC $\mathcal{D}$ in Fig. 4. The rational function for
reaching $s_{3}$ is obtained by solving the non-linear equation system:

$p_{0}=0\ \land\ p_{1}=x{\cdot}p_{2}\ \land\ p_{2}=y{\cdot}p_{1}+(1{-}y)\
\land\ p_{3}=1.$

The unique solution of this equation system yields:

$p_{0}=0\ \land\ p_{1}=\frac{x{\cdot}(1{-}y)}{1-x{\cdot}y}\ \land\
p_{2}=\frac{1{-}y}{1-x{\cdot}y}\ \land\ p_{3}=1.$

The function of pMC $\mathcal{D}$ to reach $s_{3}$ from its initial state
$s_{1}$ is thus $\frac{x{\cdot}(1{-}y)}{1-x{\cdot}y}$.

The challenge is that elimination over the ring of polynomials results in
large functions — a problem that unfortunately cannot be avoided in general.

###### Theorem 5.1

[48, 7] Computing the solution function (for reachability objectives) is
exponential in the number of parameters, and polynomial in the number of
states and the maximal degree of the polynomial transition probability
functions.

This result is a direct consequence of one-step fraction-free Gaussian
elimination. Standard Gaussian elimination does not suffice. The point is that
during triangulation, an elementary step in Gaussian elimination, the total
degree of the involved factors is doubled in the worst case. The growth of the
fractions can be often limited by eliminating common factors, i.e., by keeping
the numerator and denominator co-prime. This, however, requires computing
greatest common divisors which is expensive.444Data structures to avoid
computing gcd’s have been proposed in [49]. Fraction-free elimination avoids a
fractional representation of the intermediate matrix entries altogether. This
does not avoid the exponential growth, but in combination with the one-step
variant, it avoids gcd-computations. This keeps the coefficients during the
elimination process polynomially large. Experiments [7] indicate that this
seems beneficial for pMCs with a dense topology.

Figure 6: Small multivariate pMC with an exponentially large solution function

###### Example 6

The solution function for the family $\left(\mathcal{D}\right)_{n}$ of pMCs
with $n\geqslant 2$ parameters, $n{+}2$ states and target state $s_{n}$ in
Fig. 6 is of the form:

$\prod_{i=1}^{n}(1-x_{i})\ =\
\sum_{J\subseteq\\{1,\ldots,n\\}}-1^{|J|}\cdot\prod_{j\in J}x_{j}$

whose shortest sum-of-monomial representation has $2^{n}$ monomials.

##### State elimination.

Rather than using (one-step fraction-free) Gaussian elimination, tools such as
PARAM [40], PRISM [60] and Prophesy [33] use state elimination on the pMC as
originally proposed in [32]. This approach is analogous to computing regular
expressions from non-deterministic finite automata (NFA) [47] and has also
been applied in other contexts such as probabilistic workflow nets [34]. The
core idea behind state elimination is based on two operations:

$s$$s^{\prime}$$t$$\ldots$$\ldots$$x$$y$$1{-}x$$1{-}y$$1$$x{\cdot}(1{-}y)$

(a) before

$s$$s^{\prime}$$t$$\ldots$$\ldots$$y$$1{-}x+x{\cdot}y$$1{-}y$$1$$x{\cdot}(1{-}y)$

(b) after

Figure 7: Adding short-cuts

(1) _Adding short-cuts:_ Consider the pMC-fragment in Fig. 7(a). The
reachability probabilities from any state to $t$ are as in Fig. 7(b) where the
transitions from $s$ to $t$ via $s^{\prime}$ are replaced by a short-cut from
$s$ to $t$ and similar for all other direct successors of $s^{\prime}$, thus
bypassing $s^{\prime}$. By successively creating short-cuts, eventually any
path from the initial state to the target state consists of a single
transition.

$s$$t$$t^{\prime}$$z$$x$$y$

(a) before

$s$$t$$t^{\prime}$$\nicefrac{{x}}{{1{-}z}}$$\nicefrac{{y}}{{1{-}z}}$

(b) after

Figure 8: Self-loop removal

(2) _Eliminating self-loops:_ In order to bypass a state, it needs to be free
of self-loops. As the probability of staying forever in a non-absorbing state
$s$ is zero, self-loops at $s$ can be eliminated by rescaling all outgoing
transitions of $s$, cf. the change from Fig. 8(a) to Fig. 8(b).

As for computing regular expressions from NFA, the elimination order of states
is essential. Computing an optimal order with respect to minimality of the
result, however, is already NP-hard for acyclic NFA, see [42]. Practical
approaches resort to heuristics that are e.g., based on the pMC’s topology,
the in-degree of states, and so forth. These heuristics can be static i.e.,
once fixed for the entire computation, or dynamic in which the ordering is re-
considered during the computation depending on e.g., the complexity of
transition probability functions.

##### Experimental experiences.

Extensive experiments are reported in [51, Section 10.2]. While solution
functions can grow prohibitively large, medium-sized functions can still be
computed. E.g., for a variant of the NAND-example from the introduction with
about 300K states and 400K transitions, the solution function consisting of
4640 monomials of degree up to 200 could be computed in about 90 seconds.
Experiments also reveal that the heuristic to determine the order of state
elimination is essential and depends on the pMC at hand. For most cases, state
elimination (significantly) outperforms Gaussian elimination. Recent
experiments [72] indicate that the techniques described above significantly
outperform similar techniques used for probabilistic graphical models; e.g.,
for Bayesian network win95pts555A network with a relatively high average
Markov blanket, i.e., with relatively many causal dependencies between the
random variables. with 76 random variable and 200 parameters spread randomly
over the graph, the solution function with about 7,5 million monomials of
maximal degree 16 could be computed in about 400 seconds. It is also
beneficial to compute solution functions in a compositional way rather than on
a monolithic pMC. This has been advocated for each strongly connected
component separately [49] and more recently for more liberal decompositions of
the graphical structue of the pMC [35]. Experiments in [35] indicate possible
speed-ups of several orders of magnitude and more compact closed forms.

###  5.2 Region Verification

A direct approach to check whether $\mathcal{D},R\models\varphi$ is to use the
ETR-formulation: one exploits a satisfiability modulo theory (SMT) checker for
non-linear real arithmetic to check whether the conjunction of the ETR-formula
$F$ as described in Section 4 and a formula encoding the region $R$ is
satisfiable. The number of variables in the ETR-formula can be reduced
significantly by pre-computing the solution function using the techniques
described in the previous section. The advantage of this approach is that it
is exact and complete, but practically this SMT approach does not scale beyond
a few parameters.

###### Example 7

For the pMC in Fig. 4, this procedure amounts to check whether the ETR-formula
in Example 3 holds, or equivalently whether, phrased using the solution
function, $\frac{x{\cdot}(1{-}y)}{1-x{\cdot}y}\geqslant\nicefrac{{3}}{{4}}$
for some $0<x,y<1$.

##### A brief intermezzo: MDPs.

An alternative is to exploit a _dedicated abstraction technique_. To that end,
we require the notion of a (non-parametric) Markov decision process. Let
$\mathit{Distr}(S)$ be the set of discrete probability distributions over the
set $S$ of states.

######  Definition 2 (MDP)

A Markov decision process (MDP) is a tuple
$M=(S,s_{\mathit{I}},\mathit{Act},P)$ with a finite set $S$ of _states_ , an
_initial state_ $s_{\mathit{I}}\in S$, a finite set $\mathit{Act}$ of
_actions_ , and a (partial) _transition probability function_ $P\colon
S\times\mathit{Act}\to\mathit{Distr}(S)$.

An MDP exhibits nondeterministic choices of actions at each state, where an
action corresponds to a probability distribution over successor states, as in
Markov chains. So-called _policies_ , also referred to as schedulers or
strategies, resolve this nondeterminism. For the type of specifications in
this survey, it suffices to consider deterministic memoryless policies,
specified by $\sigma\colon S\rightarrow\mathit{Act}$. Essentially, a policy
$\sigma$ picks a unique action at each state of an MDP. Model checking for
MDPs employs techniques like value iteration or linear programming and aims to
compute the maximal or minimal probability to satisfy a specification under
any policy[69, 9]. For surveys on MDP model checking, we refer to [6, 8].

##### Parameter lifting.

Coming back to parametric models, a viable and efficient method that works for
a large class of pMCs is to transform a pMC $\mathcal{D}$ into an MDP whose
minimal (maximal) reachability probability under-approximates (over-
approximates) the reachability probability in $\mathcal{D}$ for all
instantiations in a region. The key steps of this so-called _parameter
lifting_ approach [70] are to:

  * (1)

relax the parameter dependencies (as inspired by [15]), and

  * (2)

consider lower and upper bounds of parameters as worst cases.

Put in a nutshell, it reduces a region verification query on a pMC onto a
verification query for an abstract probabilistic model, viz. an MDP
representing an interval MC [74].

$s_{0}$$s_{1}$$s_{2}$$s_{3}$$s_{4}$$x$$1{-}x$$y$$1{-}y$$y$$1{-}y$$1$$1$

(a) pMC $\mathcal{D}$

$s_{0}$$s_{1}$$s_{2}$$s_{3}$$s_{4}$

$x^{s_{0}}$

$1{-}x^{s_{0}}$

$y^{s_{1}}$

$1{-}y^{s_{1}}$

$y^{s_{2}}$

$1{-}y^{s_{2}}$

$1$$1$

(b) its relaxation

$s_{0}$$s_{1}$$s_{2}$$s_{3}$$s_{4}$$\nicefrac{{1}}{{10}}$$\nicefrac{{9}}{{10}}$$\nicefrac{{4}}{{5}}$$\nicefrac{{1}}{{5}}$$\nicefrac{{2}}{{5}}$$\nicefrac{{3}}{{5}}$$\nicefrac{{7}}{{10}}$$\nicefrac{{3}}{{10}}$$\nicefrac{{2}}{{5}}$$\nicefrac{{3}}{{5}}$$\nicefrac{{7}}{{10}}$$\nicefrac{{3}}{{10}}$$1$$1$

(c) its MDP

Figure 9: A two-phase procedure to transform a pMC into an MDP

###### Example 8

Consider the pMC $\mathcal{D}$ in Fig. 9(a) and let region
$R=[\nicefrac{{1}}{{10}},\nicefrac{{4}}{{5}}]\times[\nicefrac{{2}}{{5}},\nicefrac{{7}}{{10}}]$666More
precisely, $R=\\{v\mid
v(x)\in[\nicefrac{{1}}{{10}},\nicefrac{{4}}{{5}}],v(y)\in[\nicefrac{{2}}{{5}},\nicefrac{{7}}{{10}}]\\}$..
The parameter $y$ occurs at transitions emanating from two states. This leads
to the following trade-off. To maximise reaching the state $s_{3}$ from
$s_{1}$, the value of $y$ should be low. However, from state $s_{2}$, $y$’s
value should be large so as to avoid reaching $s_{4}$ from which $s_{3}$ is
unreachable. The optimal $y$-value depends on the probability to visit $s_{1}$
and $s_{2}$ and thus directly on $x$’s value.

(1) The first conceptual step in parameter lifting is to remove parameter
dependencies: We make all parameters occurrences unique for each state.
Parameter $y$ at state $s_{1}$ becomes $y^{s_{1}}$ and at $s_{2}$ becomes
$y^{s_{2}}$, etc. Fig. 9(b) shows the resulting pMC $\mbox{\sf
rel}(\mathcal{D})$. The corresponding 3-dimensional relaxed version of $R$ is:

$\mbox{\sf rel}(R)\ =\
\underbrace{[\nicefrac{{1}}{{10}},\nicefrac{{4}}{{5}}]}_{\text{range of
}x^{s_{0}}}\times\underbrace{[\nicefrac{{2}}{{5}},\nicefrac{{7}}{{10}}]}_{\text{range
of
}y^{s_{1}}}\times\underbrace{[\nicefrac{{2}}{{5}},\nicefrac{{7}}{{10}}]}_{\text{range
of }y^{s_{2}}}.$

On instantiating the pMC $\mbox{\sf rel}(\mathcal{D})$, the “local” copies of
$y$ get the same value. Thus, e.g.,
$(v(x),v(y))=(\nicefrac{{4}}{{5}},\nicefrac{{3}}{{5}})\in R$ becomes
$(\textsf{rel}(v)(x^{s_{0}}),\textsf{rel}(v)(y^{s_{1}}),\textsf{rel}(v)(y^{s_{2}}))=(\nicefrac{{4}}{{5}},\nicefrac{{3}}{{5}},\nicefrac{{3}}{{5}})\in\mbox{\sf
rel}(R)$. The region $\textsf{rel}(R)$ contains spurious instantiations, e.g.,
$(\nicefrac{{4}}{{5}},\nicefrac{{1}}{{2}},\nicefrac{{3}}{{5}})$, where the two
copies of $y$ have distinct values. These instantiations do not have a
counterpart in $R$. _Removing parameter dependencies is thus an over-
approximation_.

(2) The second conceptual step creates the MDP in Fig. 9(c). It has the same
state space as the pMC $\mbox{\sf rel}(\mathcal{D})$. States $s_{0}$ through
$s_{2}$ are equipped with actions for upper (lower) bounds in the region
$\mbox{\sf rel}(R)$, indicated by solid (dashed) lines. For instance, state
$s_{2}$ has a solid (dashed) transition with probability
$\nicefrac{{7}}{{10}}$ ($\nicefrac{{2}}{{5}}$) to $s_{1}$. These transitions
represent the largest (smallest) probability to go from $s_{2}$ to $s_{1}$ in
$\mbox{\sf rel}(R)$. As each value between these two extreme values can be
selected, the resulting MDP is in fact an interval MC [74]. Choices in $s_{3}$
and $s_{4}$ are unique, as the outgoing transitions in $\mbox{\sf
rel}(\mathcal{D})$ are constant.

How is an analysis of the resulting MDP related to checking whether
$\mathcal{D},R\models\varphi$? Assume that $\varphi$ requires to reach state
$s_{3}$ with at most probability $\nicefrac{{4}}{{5}}$, i.e.,
$\nicefrac{{48}}{{60}}$. Verifying the resulting MDP using standard
probabilistic model checking (PMC) techniques [55, 6, 8] yields a maximal
probability to reach $s_{3}$ of $\nicefrac{{47}}{{60}}$. This is achieved by a
policy that selects solid transitions in $s_{0}$ and $s_{2}$ and dashed
transitions in $s_{1}$. As
$\nicefrac{{47}}{{60}}\leqslant\nicefrac{{48}}{{60}}$, and the MDP over-
approximates pMC $\mathcal{D}$, it follows that $\mathcal{D},R\models\varphi$.
If $\varphi$ would impose a lower bound (rather than an upper bound) on the
reachability objective, the minimal probability to reach $s_{3}$ in the MDP is
considered.

##### Correctness.

For the following result, we use the notion of the Markov chain $M^{\sigma}$
that is _induced_ by an MDP $M$ and a policy $\sigma$.

###### Theorem 5.2

[70] Let $\mathcal{D}$ be a locally monotone pMC, $R$ a rectangular and closed
region777A rectangular and closed region is of the form
$\prod_{i}[\ell_{i},u_{i}]$ where the value of parameter $x_{i}$ lies in the
closed interval $[\ell_{i},u_{i}]$., $\varphi$ a reachability specification,
and $M$ the resulting MDP from lifting $\mathcal{D}$ and $R$. Then:

  1. 1.

(for all policies $\sigma$ on $M$: $M^{\sigma}\models\varphi$) implies
$\mathcal{D},R\models\varphi$, and

  2. 2.

(for all policies $\sigma$ on $M$: $M^{\sigma}\models\neg\varphi$) implies
$\mathcal{D},R\models\neg\varphi,$

where $\sigma$ ranges over all possible policies for the MDP $M$.

Note that the (graph-preserving) region $R$ is required to be rectangular and
closed, and that pMC $\mathcal{D}$ is locally monotone, i.e., the transition
probability functions in $\mathcal{D}$ are monotonic. Examples of such
functions are e.g., multi-linear polynomials. The first constraint makes the
bounds of the parameters independent of other parameter instantiations and
ensures the maximum (and minimum) over the region $R$ to exist. Due to the
local monotonicity and the absence of parameter dependencies after relaxation,
maximal reachability probabilities are easy to determine: it suffices to
consider instantiations that set the value of each parameter to either the
lowest or highest possible value. These two constraints on $\mathcal{D}$ and
$R$ are quite mild; in fact, almost all examples from the literature comply to
these constraints.

##### Region refinement.

If the over-approximation $\mbox{\sf rel}(R)$ of region $R$ is too coarse for
a conclusive answer, $R$ can be refined into smaller regions. Intuitively, by
excluding more potential parameter values, the actual choice of the parameter
value has lesser impact on reachability probabilities. The smaller the region,
the smaller the over-approximation: the optimal instantiation on the pMC
$\mathcal{D}$ is over-approximated by some policy on the MDP $M$. The
approximation error originates from choices where an optimal policy on $M$
chooses actions $v_{1}$ and $v_{2}$ at states $s_{1}$ and $s_{2}$,
respectively, with $v_{1}(x_{i}^{s_{1}})\neq v_{2}(x_{i}^{s_{2}})$ for some
parameter $x_{i}$, and therefore intuitively disagree on its value. The
probability mass that is affected by these choices decreases if the region is
smaller.

##### Experimental results.

Experiments [70, 51] show that parameter lifting is an excellent approach for
region verification if the influence of the parameter dependencies is minor,
or if the number of parameters is relatively low (at most 15, say). For more
parameters, the refinement in exponentially many regions often yields a
prohibitive number of sub-regions that have to be analysed.

The beauty of parameter lifting is threefold: (1) it is conceptually simple,
(2) its principle is applicable to other models such as parametric MDPs (which
are then transformed into two-player stochastic games), and (3) it reduces a
verification problem on parametric probabilistic models to a model-checking
query on non-parametric probabilistic models for which efficient algorithms
exist.

###  5.3 Approximate Parameter Space Partitioning

The approximate parameter space partitioning problem requests to partition
region $R$ into accepting and rejecting fragments together with an unknown
fragment which covers at most fraction $1{-}\eta$ of $R$’s volume. This
section presents an iterative approach to this problem that builds on top of
region verification discussed just above. The basic idea of this approach was
first presented in [33] and has substantially been refined and extended in
[50, Ch. 8].

##### The basic idea.

Approximate parameter space partitioning can be viewed as a _counter-example
guided abstraction_ refinement (CEGAR)-like [27] approach to successively
divide the parameter space into accepting and rejecting regions. The basic
idea is to compute a sequence $\left(R^{i}_{+}\right)_{i\in\mathbb{N}}$ of
simple (read: rectangular) accepting regions that successively extend each
other. Similarly, an increasing sequence
$\left(R^{i}_{-}\right)_{i\in\mathbb{N}}$ of simple rejecting regions is
computed. At the $i$-th iteration, $R^{i}=R^{i}_{+}\cup R^{i}_{-}$ is the
covered fragment of the parameter space. The iterative approach halts when
$R^{i}$ covers at least $100{\cdot}\eta$% of the entire region $R$.
Termination is guaranteed: in the limit a solution to the exact synthesis
problem is obtained as $\lim_{i\rightarrow\infty}R_{+}^{i}=R_{+}$ and
$\lim_{i\rightarrow\infty}R_{-}^{i}=R_{-}$.

Issues are e.g., how to find good region candidates, how to refine a region,
and how to effectively use diagnostic feedback if a region is found to be
inconclusive.

######  Example 9 (A naive procedure)

Consider the parametric die from Example 1. Suppose we want to synthesise the
partitioning in Fig. 3 on page 3. We start by verifying the full parameter
space $R$ against $\varphi$. The verifier returns false, as $R$ is not
accepting. Since $R$ might be rejecting, we invoke the verifier with $R$ and
$\neg\varphi$, yielding false too. Thus, the full parameter space $R$ is
inconclusive. Let us now split $R$ into four equally-sized regions, all of
which turn out to be inconclusive. Only after splitting again by the same
principle, the first accepting and rejecting regions are found. After various
iterations, this procedure leads to the partitioning in Fig. 3.

##### Finding region candidates.

Rather than starting with the entire (typically large and inconclusive)
initial region $R$, a better strategy is to first do some _sampling_. Here,
sampling means identifying an instantiation $v\in R$ and verifying using an
off-the-shelf probabilistic model checker for MCs whether
$\mathcal{D}[v]\models\varphi$. One can e.g., start by uniformly sampling the
region $R$, see Fig. 10(a). A red cross at point $v=(v(x),v(y))$ indicates
that $\mathcal{D}[v]\models\neg\varphi$, while a green dot indicates
$\mathcal{D}[v]\models\varphi$. The sampling results can be used to steer the
selection of a candidate region that is consistent with all samples contained
in it; e.g., the blue rectangle in Fig. 10(a) is a candidate region for the
hypothesis $\neg\varphi$ (indicated by the hatching) as it only contains red
crosses.

(a) (Uniform) sampling

(b) Generating candidates

(c) Preliminary result

Figure 10: Parameter space partitioning in progress (using PROPhESY [33].)

##### How to split regions?

A simple strategy is to split regions that sampling or region verification
revealed to be inconsistent.

###### Example 10

After several iterations, the iterative refinement proceeded to the situation
in Fig. 10(b). The blue candidate region in Fig. 10(a) turned out to be not
rejecting; the region verifier provided the counterexample
$(p,q)=(0.45,0.52)$. Further iterations with smaller regions had some success,
but some additional samples (the dots and circles that are off-grid points)
were obtained as counterexamples. The blue region in Fig. 10(b) is a candidate
for $\varphi$. Fig. 10(c) shows a further snapshot indicating that this blue
candidate region is indeed accepting. The white box on the right border has
been checked but its verification timed out without any counterexample.

Splitting of regions based on the available samples can be done in various
ways, e.g., by splitting regions into equally-sized regions (as used in the
above example), or by attempting to gradually obtain larger candidates. The
rationale of the former is to obtain small regions with small bounds whereas
the latter is based on the rationale to quickly cover a vast fragment of the
parameter space. For the construction of region candidates, a good practical
strategy is to split the initial regions according to a heuristic until none
of the regions is inconclusive. Candidate regions are sorted in descending
size. Regions are preferred where verification seems less costly: candidate
regions that are supposed to be accepting and are further away from samples or
regions that are rejecting are preferred over those regions which have
rejecting samples or are close to rejecting regions.

(a) Herman’s model

(b) NAND model

Figure 11: Covered parameter space during partitioning for two benchmarks

##### Experimental experiences.

Fig. 11(a) depicts results for parameter space partitioning on Herman’s
randomised self-stabilisation algorithm [45] for a distributed system with
five processes and threshold $\lambda=5$. This model has one parameter, 33
states and 276 transitions. The plot depicts the covered parameter space for
three techniques with both quads (straight lines) and rectangles (dashed
lines) as region representations. A point $(x,y)$ indicates that $y$ percent
of the parameter space could be covered within $x$ seconds. The three
techniques are parameter lifting (PLA), the ETR-encoding, and the solution
function (SF) encoded as ETR-formula. Recall that the ETR-encoding contains a
variable for each state and each parameter, whereas the SF only contains a
variable for each parameter, cf. equation (1).

Figure 12: Approximate parameter partitioning on three Bayesian networks with
each eight parameters

For Herman’s distributed algorithm, SMT-based techniques perform better than
PLA. PLA was able to cover 64% of the parameter space within milliseconds but
only 2% more space was covered in the remaining hour. SMT was able to cover at
least 99% of the parameter space within 15 seconds. Moreover, rectangles cover
the parameter space faster than quads. The results on the NAND model [44] are
a bit different, see Fig. 11(b). This model has two parameters, 178 states and
243 transitions. Here, PLA outperforms SMT. Rectangles and quads perform on
par, although for smaller thresholds their performance does differ.
Applications on various benchmarks reveals that parameter lifting is almost
always superior but not on all benchmarks and all (sub-)regions. There can be
substantial differences between the heuristics for candidate generation,
especially in settings where single region verification calls are expensive.
To indicate the scalability of the approach, we report on some recent
experiments [73] on parametric Bayesian networks. Figure 12 shows that 80-90%
of the 8-dimensional parameter space for three parametric Bayesian networks
(win95pts, hailfinder, and hepar-2) can be covered in about 100-1,000 seconds.

###  5.4 Feasibility Checking

We now return to the ETR-complete feasibility problem of before and describe
how techniques from mathematical optimisation can be exploited to obtain a
scalable approach.

##### Two “extreme” approaches: sampling and ETR-solving.

To find a satisfiable parameter instantiation it suffices to guess an
instantiation $v$ such that $\mathcal{D}[v]\models\varphi$. Checking whether
$\mathcal{D}[v]\models\varphi$ can be done using PMC techniques [55, 6] or,
alternatively, by instantiating the solution function efficiently [37]. This
insight has led to an adaptation of sampling-based techniques to the parameter
synthesis problem, most prominently particle swarm optimisation (PSO) [24].
These techniques can handle millions of states but their efficiency is limited
for models with more than roughly ten parameters, see the left part of Fig.
13. Rather than pure sampling-based techniques such as PSO, one can pursue an
exact (but costly) approach by computing the ETR-formula and checking whether
it is satisfiable. This is exact, but costly as indicated on the right part of
Fig. 13.

##### A middle ground: mathematical optimisation.

An approach that is suitable compromise between sampling and exact solution
techniques is to exploit techniques from _mathematical optimisation_. The
basic idea is to guess a parameter instantiation $v$, and then optimise around
this $v$ in the parameter space so as to find a point that improves the
reachability probability (or whatever specification we are interested in) in
the induced MC. This is repeated until an accepting instantiation is found.
Rather than optimising on the original ETR formula, the formula is
approximated such that every iteration step is computationally tractable. This
idea can be realised using different ideas. These ideas share that they
exploit the model structure of the pMC $\mathcal{D}$, and need fewer
iterations than sampling-based methods. Differences occur due to the choice of
approximation, e.g., the problem can be convexified [29] or linearised [30].
Although we consider pMCs, this technique is also applicable to parametric
MDPs.

Figure 13: Comparing various techniques for feasibility for different levels
of precision

##### Feasibility as an optimisation problem.

The first step is to formulate the feasibility problem as an optimisation
problem. Assuming that all transition probabilities are linear in the
parameters, the ETR-formula can be represented as a _quadratically-constrained
quadratic program_ (QCQP [14]), an optimisation problem with a quadratic
objective that is to be achieved under a set of quadratic constraints888For
readers familiar with the LP encoding for reachability objectives for MDPs,
this QCQP is the straightforward representation of this LP where the
transition probabilities (parameters) are multiplied with the state-
variables.. We show this for a key part of the ETR encoding:

$\displaystyle\begin{split}&\text{minimise }p_{s_{\mathit{I}}}\text{
s.t.}\quad\\\ &p_{s}\ \geqslant\ \sum_{s^{\prime}\in
S_{>0}}\underbrace{\mathcal{P}(s,s^{\prime})\cdot
p_{s^{\prime}}}_{=\,h(s,s^{\prime})}\quad\text{for all }s\in S_{>0}\setminus
G,\end{split}$ (3)

where $S_{>0}$ and $G\subseteq S$ are as before in Eq. (2). Note that the QCQP
formulation is exact: its solutions coincide with the solutions to the ETR-
formulation. However, in general, the QCQP is a non-convex optimisation
problem — witnessed by the encoding of the pMC in Fig. 14 — and thus not
directly amenable to efficient methods (which is a trivial consequence of the
ETR-completeness of the problem).

Figure 14: A sample pMC to illustrate the use of mathematical optimisation

###### Example 11

The ETR constraints for the pMC in Fig. 14 to reach state $s_{3}$ with
threshold $\leqslant\lambda$ are:

$p_{0}\leqslant\lambda,\quad\varepsilon\leqslant x\leqslant
1{-}\varepsilon,\quad p_{3}=1,\quad p_{0}\geqslant x{\cdot}p_{1},\quad
p_{1}\geqslant(1{-}x){\cdot}p_{2},\quad p_{2}\geqslant x{\cdot}p_{3}.$

Quadratic constraints are e.g., $(1{-}x){\cdot}p_{2}$ and $x{\cdot}p_{1}$.

##### Turning the QCQP into a series of LP problems.

We present a _sequential-convex-optimisation_ (SCP) approach that iteratively
solves LPs to find a solution of the QCQP. This approach is originally
presented in [85, 62, 25] and has been adapted for pMCs in [30]. Eventually,
the solution of one of these LPs will provide a solution to the original QCQP.
Checking whether this is indeed the case can be done by model checking the
instantiated pMC. Given an assignment $\hat{v}$ to $v$, we obtain an affine
approximation in the form of a linearisation $\hat{f}$ of the polynomial $f$
around $\hat{v}$:

$\hat{f}_{\hat{v}}\ =\ f[\hat{v}]+\nabla f[\hat{v}]^{T}\cdot(v-\hat{v})$ (4)

where $\nabla f[\hat{v}]$ is the gradient of the polynomial $f$ at $\hat{v}$.
Consequently, the LP approximation around $\hat{v}$ of the constraint
(LABEL:eq:etr-encoding) then reads:

$p_{s}\ \geqslant\ \sum_{s^{\prime}\in
S_{>0}}h_{\hat{v}}(s,s^{\prime})\quad\text{for all }s\in S_{>0}\setminus G.$

However, the LP from the conjunction of these variables is not necessarily
feasible. To remedy this, we relax the LP by introducing a penalty variable
$k_{s}$ for each state $s$ that intuitively allows violating the constraints
up to some degree. By adapting the objective function, we encourage the solver
to not violate the constraints, turning (LABEL:eq:etr-encoding) into:

$\displaystyle\begin{split}&\text{minimise
}p_{s_{\mathit{I}}}+\tau{\cdot}\sum_{s}k_{s}\text{ s.t.}\quad\\\ &k_{s}+p_{s}\
\geqslant\ \sum_{s^{\prime}\in S_{>0}}h_{\hat{v}}(s,s^{\prime})\quad\text{for
all }s\in S_{>0}\setminus G.\end{split}$ (5)

The constant $\tau$ is chosen sufficiently large. To ensure that the
linearisation is accurate, we enforce that the solution is sufficiently close
to $\hat{v}$ using _trust regions_ [85].

###### Example 12

After a linearisation around an assignment for the parameter instantiation
$\hat{x}$, $\hat{p_{0}}$ through $\hat{p_{2}}$, the resulting LP formulation
for our example pMC requires to minimise $p_{0}+\tau\cdot\sum k_{i}$ under
$k_{i}\geqslant 0$, $p_{3}=1$, $p_{0}\leqslant\lambda$, and the linear
constraints:

$\begin{array}[]{rcl}k_{0}+p_{0}&\
\geqslant&\hat{x}{\cdot}\hat{p_{1}}+\hat{p_{1}}{\cdot}(x{-}\hat{x})+\hat{x}{\cdot}(p_{1}{-}\hat{p_{1}})\\\\[4.30554pt]
k_{1}+p_{1}&\geqslant&p_{2}-\hat{x}{\cdot}\hat{p_{2}}-\hat{p_{2}}{\cdot}(x{-}\hat{x})-\hat{x}{\cdot}(p_{2}{-}\hat{p_{2}})\\\\[4.30554pt]
k_{2}+p_{2}&\geqslant&\hat{x}{\cdot}\hat{p_{3}}+\hat{p_{3}}{\cdot}(x{-}\hat{x})+\hat{x}{\cdot}(p_{3}{-}\hat{p_{3}}),\end{array}$

and some constraints on the trust region with radius $\delta>0$, where
$\delta^{\prime}=\delta{+}1$:

$\nicefrac{{\hat{p_{0}}}}{{\delta^{\prime}}}\geqslant
p_{0}\geqslant\hat{p_{0}}{\cdot}\delta^{\prime},\ \
\nicefrac{{\hat{p_{1}}}}{{\delta^{\prime}}}\geqslant
p_{1}\geqslant\hat{p_{1}}{\cdot}\delta^{\prime},\ \
\nicefrac{{\hat{p_{2}}}}{{\delta^{\prime}}}\geqslant
p_{2}\geqslant\hat{p_{2}}{\cdot}\delta^{\prime},\text{ and
}\nicefrac{{\hat{x}}}{{\delta^{\prime}}}\geqslant
x\geqslant\hat{x}{\cdot}\delta^{\prime}.$

##### Integration with probabilistic model checking.

These methods can ensure the correctness of the solution only when the initial
point is feasible, which amounts to solving the parameter synthesis problem.
Thus, this assumption cannot be made. Instead, we employ the following scheme.
A PMC step is integrated into the SCP approach, see details in [30] to verify
whether the instantiated pMC by the solutions for $x$, $v=\textrm{res}(x)$,
obtained from the LP improves upon the previous instantiation. If indeed the
computed reachability probability from the initial state (by convention:
$\textrm{res}(p)_{0}$) increases over the result ($\beta$) from the previous
iteration, then these values are used in the next iteration. Otherwise, the
radius of the trust region is contracted (by a factor $\gamma<1$) and the LP
is solved again. If the trust region becomes too large ($>\omega$), we may
have hit a local optimum and restart. A schematic overview of the resulting
iterative procedure is given in Fig 15.

convexify
---
around $\hat{v},\hat{p}$
make initial
---
guess $\hat{v},\hat{p}$,
$\beta\leftarrow 0$
solve
---
LP
model check
---
the MC:
$\mathcal{D}[v]\models\varphi$
$\textrm{res}(p)_{0}>\beta$update: $\hat{v}\leftarrow
v$,$\hat{p}\leftarrow\textrm{res}(p),$$\delta\leftarrow\delta\cdot\gamma$,$\beta\leftarrow\textrm{res}(p)_{0}$update:
$\delta\leftarrow\delta/\gamma$$\delta>\omega$$\mathcal{D},\varphi$ return
---
$v$
restart$\textrm{res}(p)$$v$LPyesnoyesnoyesno Figure 15: Feasibility checking
using an integrated SCP-PMC approach

Trust region methods converge under regularisation assumptions such as
Lipschitz continuity for the gradients of the functions in the objective and
constraints. These conditions are satisfied for our QCQP formulation.

##### What is different in CCP?

Above, we outlined the SCP approach from Fig. 13. The figure also mentions the
CCP procedure, which approximates the QCQP using a series of convex programs
rather than a series of linear programs. The main trick is to write the
quadratic terms as a sum of a convex and a concave part, and then to linearise
the concave part. Contrary to the SCP approach, this construction ensures that
the constraints all (in some sense) overapproximate the original solution, and
thus that (whenever the penalty variables are assigned to zero) a solution to
the convexified QCQP is a solution to the original QCQP.

##### Experimental evaluation.

Experiments [30] on several benchmarks indicate that the SCP-PMC technique can
solve feasibility for pMCs with hundreds of thousands of states and tens of
thousands of parameters. Why not use plain SCP? The integration of PMC
techniques yields an improvement of multiple orders of magnitude in run time
compared to plain SCP, and guarantees the solution’s correctness.

##  6 Controller Synthesis under Partial Observability

As indicated in the introduction of this survey, the feasibility problem for
parametric MCs — find a parameter instantiation satisfying reachability
objective $\varphi$ — is equivalent to the finite-memory controller synthesis
problem for $\varphi$ in POMDPs. A POMDP is in fact a finite-state MDP in
which to each state a set of observations is associated. States with the same
observations have the same set of enabled actions.

A policy for a POMDP, e.g., to maximise the probability to eventually reach a
given state, has to base its decisions on the sequence of observations seen so
far. This contrasts policies for MDPs that have the sequence of states visited
so far at their disposal to make a decision. Deciding whether there exists an
observation-based policy satisfying an infinite-horizon reachability
specification $\varphi$ is undecidable [61]. Optimal policies need infinite
memory. For computational tractability, policies are therefore often
restricted to finite memory and are randomised: an enabled action is taken
with some probability. Let us for simplicity restrict ourselves to memory-less
(aka: positional) policies. These policies have memory size one.

###### Theorem 6.1

[52] The decision problem whether there exists a memory-less policy for a
POMDP satisfying $\varphi$ is polynomial-time equivalent to the feasibility
checking problem for $\varphi$ on a corresponding pMC.

$s_{0}$$s_{2}$$s_{1}$$s_{3}$$\alpha_{1}$$\alpha_{2}$$\alpha_{3}$$\alpha_{1}$$\alpha_{2}$$\alpha_{1}$$\alpha_{2}$$1$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$1$$1$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$1$$1$

(a) A sample POMDP

$s_{0}$$s_{2}$$s_{1}$$s_{3}$${\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}x_{1}}\cdot
1$${\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}x_{2}}\cdot\nicefrac{{1}}{{2}}$${\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}x_{3}+x_{2}}\cdot\nicefrac{{1}}{{2}}$$\color[rgb]{1,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.4,0.4}y_{2}$$\color[rgb]{1,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.4,0.4}y_{1}$$\nicefrac{{1}}{{2}}\cdot{\color[rgb]{1,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.4,0.4}y_{2}}$
${\color[rgb]{1,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.4,0.4}y_{1}}+\nicefrac{{1}}{{2}}\cdot{\color[rgb]{1,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.4,0.4}y_{2}}$$1$

(b) Its corresponding pMC

Figure 16: The connection between POMDPs and pMCs

Together with Theorem 4.1, this yields that finding a policy for a POMDP
satisfying $\varphi$ is ETR-complete. This improves the known complexity
results for the POMDP controller synthesis decision problem: being NP-hard,
SQRT-SUM-hard and being in PSPACE [81]. How to obtain a corresponding pMC? One
can obtain a pMC for a POMDP under an arbitrary randomised memory-less policy
in a simple way. The topology of the pMC and POMDP are identical. The
parametric transition probabilities in the pMC are obtained from the (unknown)
probabilities to select actions in the POMDP by an arbitrary randomised
policy. The following example illustrates this for a memory-less policy.

###### Example 13

Fig. 16(a) depicts a sample POMDP where colors indicate the observations at a
state, and actions are indicated by $\alpha_{i}$. Now consider the following
memory-less randomised policy. In any red colored state, it takes action
$\alpha_{1}$ with probability $y_{1}$, and action $\alpha_{2}$ with
probability $y_{2}$. At any blue colored state, action $\alpha_{i}$ is taken
with probability $x_{i}$. This perspective directly yields the pMC of Fig.
16(b).

The connection and construction for memory-less policies can be extended to
finite-memory controllers. We employ randomised finite-state controllers
(FSCs) [67], that are essentially extensions of Moore machines. A POMDP
satisfies $\varphi$ under some $k$-FSC (an FSC with $k$ memory states) if and
only if a POMDP that is obtained by a $k$-_unfolding_ of the original POMDP
satisfies $\varphi$ under a memory-less policy. This unfolding can be viewed
as the synchronous product construction of the POMDP and the $k$-FSC. The
induced pMC of the unfolded POMDP has a state space that is linear in $k$ and
its number of parameters is quadratic in $k$ and linear in the total number of
observations as well as the maximal number of actions over all observations.

Figure 17: Satellite trajectories obtained by pMC feasibility checking

##### A satellite collision avoidance example.

We consider a swarm of satellites following circular orbits with a radius of
7728 km. A satellite can follow its current trajectory with no fuel usage. A
trajectory is discretised in numerous (7200) time steps. Based on regularly
obtained observations, at every observation the satellite can either stay in
its current trajectory or can switch to a close ($\leqslant$ 250 km apart)
trajectory. In total 36 trajectories are possible. The objective is to compute
a switching policy that ensures the satellite to avoid collisions with other
objects with high (0.995) probability. The POMDP for this scenario ranges from
6K states and a few hundred observations for $k{=}0$ (memory-less) to 288K
states and thousands of observations for $k{=}5$. The feasibility of the
resulting pMC is analysed using the SCP-PMC approach from Section 5.4. Figure
17 indicates the obtained policies for a memory-less policy (left) and a
policy with memory size five (right) obtained in about 20 seconds and five
minutes of computation time respectively. The initial satellite position is
indicated by a fat red circle. The black spheres represent the obstacles to be
avoided. The average length of the trajectory with the finite-memory policy is
about half the length for the for the memory-less policy.

##  7 Epilogue

Finally, we present some interesting research directions on parameter
synthesis along with some first results in these directions.

#### Monotonicity checking.

It is often the case that perturbing parameter values has a monotonic
influence on the induced reachability probability. Consider, e.g., a network
protocol where increasing the channel quality typically decreases the
protocol’s packet drop rate. Increasing parameter values that encode the
reliability of hardware components will typically increase the system’s
reliability. The decision problem whether the reachability probability
function is monotonic in a given parameter is however ETR-hard [77].
Nevertheless, checking sufficient properties on the topology of the pMC yields
effective methods to establish monotonicity [77]. Whenever monotonicity (in
some parameter) is established, region verification and feasibility checking
become significantly cheaper. In general, however, the overhead of first
establishing monotonicity does not always pay off.

Recently, [78] intertwined the region verification method outlined in Section
5.2 with establishing monotonicity (within that region). The main benefit is
that when the over-approximation of the region verification is too coarse, the
obtained bounds from the verification help to establish monotonicity whereas
on the other hand monotonicity results simplify the refinement loop in region
verification. This yields an effective method to solve the _optimal_ 999In
fact, $\varepsilon$-optimal feasibility, i.e., finding a parameter
instantiation that achieves the maximal or minimal reachability probability up
to a given accuracy $\varepsilon>0$. feasibility problem.

When assuming monotonicity, hill climbing (gradient descent, GD) methods for
feasibility checking perform especially well: the optimal value will be in a
corner of the parameter space and the GD methods will accelerate sampling
towards that corner. We furthermore observe that the performance here neither
requires establishing monotonicity a priori, nor does it require monotonicity
in all parameters. The key step to enable GD methods is to efficiently compute
the gradient. The recent paper [76] shows that this is possible and
additionally empirically compares various GD methods in the context of
feasibility checking.

#### Transfer to other models.

Various approaches in this survey carry over to parametric MDPs101010Solution
functions for pMDPs are challenging, but can be thought of as the maximum over
the solution functions for the induced pMCs.. This applies e.g., to complexity
results for feasibility, parameter lifting, and mathematical optimisation for
feasibility. Various works consider even richer models. In particular, the
methods described here can be extended towards parametric probabilistic timed
automata [43] and to controller synthesis for uncertain POMDPs, see below.
Similarly, there exist various approaches for parametric continuous-time MCs,
see, e.g., [18, 16, 39] and parameter synthesis has been applied to stochastic
population models [41] and to accelerate solving hierarchical MDPs [54].

Beyond Markov models, probabilistic graphical models in general and Bayesian
networks in particular are widespread to describe complex conditional
probability distributions. Recent work [72, 73] shows that ideas and methods
for parameter synthesis in Markov chains as described in this survey
significantly improve upon existing methods for parametric Bayesian networks
[21]. Vice versa, some inference techniques do yield interesting alternatives
for the analysis of (finite-horizon properties in) pMCs [46].

Synthesis techniques explained in this survey are also used for stochastic
hybrid systems. The approach advocated in [65] takes a parametric stochastic
differential equation (SDE) and a specification $\varphi$, computes a
parametric formal abstraction, yielding a (parametric) abstract model, and
synthesises parameters on the abstract model in order to satisfy $\varphi$ for
the SDE. The abstraction can be iteratively refined to increase its precision.

Parameter synthesis has recently also been considered for the richer type of
probabilistic hyper-properties [1], properties that are relevant in e.g.,
security.

#### Topology synthesis.

The methods presented here are tailored towards continuous parameter values
with a continuous solution function (which means that most methods assume
graph-preserving regions or acyclic pMCs). A related setting studies discrete
parameters and varying topologies. Such settings naturally occur when
synthesising implementations of probabilistic programs and controllers in
probabilistic settings. In a nutshell, methods rely either on abstraction-
refinement [20], similar to Section 5.2, or on inductive synthesis [19]
inspired by ideas such as programming-by-example and program synthesis. These
two methods can be efficiently combined [2]. Despite a slightly different
focus, the integration of the discrete and continuous setting seems a natural
next step.

#### Variations.

Beyond the problem statements discussed in this paper, there are various
related problem statements.

##### Robust policies.

For parametric MDPs, one can either quantify:

  * •

(_robust policies_) first over the policies and then over the parameters, or

  * •

(_robust parameters_) first over the parameters and then over the policies.

The generalisation of the approaches in this paper consider the latter. While
some ideas carry over, there are some differences. Furthermore, finding
memory-less robust policies is theoretically harder than finding robust
parameters and, in general, optimal robust policies require memory [53, 3]. We
remark that the notion of robustness itself can also be considered on pMCs,
using, e.g., perturbation analysis [23].

##### Interval and other uncertainty models.

Many models assume a more local notion of uncertainty in transition
probabilities. Typically, the verification problem for such models aims at
robustness against all probability distributions within the uncertainty sets;
this may also mean robust policies as discussed above. The transitions of
uncertain MCs or MDPs are equipped with, e.g., _probability intervals_ ,
_likelihood functions_ , or form even more general uncertainty sets [10, 68,
38, 84, 63, 59]. For a detailed handling of different types of uncertainty
sets, we refer to [83]. Extensions to uncertain POMDPs also exist [79, 31].

##### Distributions over parameters.

Rather than assuming the best or worst case for parameter values, one can
equip parameters with a parameter distribution [3]. For pMCs, this assumption
then enables sampling-based approaches that yield probably-approximately-
correctness (PAC) style guarantees [4]. Finally, one may integrate Bayesian
updates on parameter distributions with the analysis of pMCs [66]. For
parametric continous-time MCs, both scenario-based approaches [5] and a
variety of approaches around Gaussian processes exist [12, 13].

##### Model repair and optimisation.

Parameter synthesis plays an important role in model repair [11, 64]: how can
the transition probabilities in a given parameter-less MC that refutes a given
specification $\varphi$ be changed such that an MC is obtained satisfying
$\varphi$? Model repair reduces to a feasibility checking problem. To deal
with large state spaces, model repair has been combined with abstraction [22].
Optimal feasibility has been applied to find the optimal bias of coin flips
used in self-stabilisation algorithms for distributed systems [82].

### Acknowledgements

We thank all our co-authors in the work(s) surveyed in this paper: Erika
Ábrahám, Christel Baier, Bernd Becker, Harold Bruintjes, Florian Corzilius,
Murat Cubuktepe, Christian Hensel, Lisa Hutschenreiter, Joachim Klein,
Guillermo Pérez, Tim Quatmann, Ufuk Topcu, Matthias Volk, Ralf Wimmer, Tobias
Winkler and Leonore Winterer. We thank Bahare Salmani, Jip Spel, and Tobias
Winkler as well as the reviewers of this volume for their thoughtful feedback
on a draft version of this survey.

## References

  * [1] Ábrahám, E., Bartocci, E., Bonakdarpour, B., Dobe, O.: Parameter synthesis for probabilistic hyperproperties. In: LPAR. EPiC Series in Computing, vol. 73, pp. 12–31. EasyChair (2020)
  * [2] Andriushchenko, R., Ceska, M., Junges, S., Katoen, J.P.: Inductive synthesis for probabilistic programs reaches new horizons. In: TACAS (1). LNCS, vol. 12651, pp. 191–209. Springer (2021)
  * [3] Arming, S., Bartocci, E., Chatterjee, K., Katoen, J.P., Sokolova, A.: Parameter-independent strategies for pMDPs via POMDPs. In: QEST. LNCS, vol. 11024, pp. 53–70. Springer (2018)
  * [4] Badings, T.S., Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Scenario-based verification of uncertain parametric MDPs. Int. J. Softw. Tools Technol. Transf. (2022), to appear
  * [5] Badings, T.S., Jansen, N., Junges, S., Stoelinga, M., Volk, M.: Sampling-based verification of CTMCs with uncertain rates. In: CAV (2022), to appear
  * [6] Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963–999. Springer (2018)
  * [7] Baier, C., Hensel, C., Hutschenreiter, L., Junges, S., Katoen, J.P., Klein, J.: Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. Inf. Comput. 272, 104504 (2020)
  * [8] Baier, C., Hermanns, H., Katoen, J.P.: The 10,000 facets of MDP model checking. In: Computing and Software Science, LNCS, vol. 10000, pp. 420–451. Springer (2019)
  * [9] Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)
  * [10] Bart, A., Delahaye, B., Fournier, P., Lime, D., Monfroy, E., Truchet, C.: Reachability in parametric interval Markov chains using constraints. Theor. Comput. Sci. 747, 48–74 (2018)
  * [11] Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: TACAS. LNCS, vol. 6605, pp. 326–340. Springer (2011)
  * [12] Bortolussi, L., Milios, D., Sanguinetti, G.: Smoothed model checking for uncertain continuous-time Markov chains. Inf. Comput. 247, 235–253 (2016)
  * [13] Bortolussi, L., Silvetti, S.: Bayesian statistical parameter synthesis for linear temporal properties of stochastic models. In: TACAS. LNCS, vol. 10806, pp. 396–413. Springer (2018)
  * [14] Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge Univ. Press (2004)
  * [15] Brim, L., Ceska, M., Drazan, S., Safránek, D.: Exploring parameter space of stochastic biochemical systems using quantitative model checking. In: CAV. LNCS, vol. 8044, pp. 107–123. Springer (2013)
  * [16] Calinescu, R., Ceska, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: Efficient synthesis of robust models for stochastic systems. J. Syst. Softw. 143, 140–158 (2018)
  * [17] Canny, J.F.: Some algebraic and geometric computations in PSPACE. In: STOC. pp. 460–467. ACM (1988)
  * [18] Ceska, M., Dannenberg, F., Kwiatkowska, M.Z., Paoletti, N.: Precise parameter synthesis for stochastic biochemical systems. In: CMSB. LNCS, vol. 8859, pp. 86–98. Springer (2014)
  * [19] Ceska, M., Hensel, C., Junges, S., Katoen, J.P.: Counterexample-driven synthesis for probabilistic program sketches. In: FM. LNCS, vol. 11800, pp. 101–120. Springer (2019)
  * [20] Ceska, M., Jansen, N., Junges, S., Katoen, J.P.: Shepherding hordes of Markov chains. In: TACAS (2). LNCS, vol. 11428, pp. 172–190. Springer (2019)
  * [21] Chan, H., Darwiche, A.: When do numbers really matter? J. Artif. Intell. Res. 17, 265–287 (2002)
  * [22] Chatzieleftheriou, G., Katsaros, P.: Abstract model repair for probabilistic systems. Inf. Comput. 259(1), 142–160 (2018)
  * [23] Chen, T., Feng, Y., Rosenblum, D.S., Su, G.: Perturbation analysis in verification of discrete-time markov chains. In: CONCUR. LNCS, vol. 8704, pp. 218–233. Springer (2014)
  * [24] Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: TASE. pp. 85–92. IEEE Computer Society (2013)
  * [25] Chen, X., Niu, L., Yuan, Y.: Optimality conditions and a smoothing trust region Newton method for non-Lipschitz optimization. SIAM J. Optim. 23(3), 1528–1552 (2013)
  * [26] Chonev, V.: Reachability in augmented interval Markov chains. CoRR abs/1701.02996 (2017)
  * [27] Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV. LNCS, vol. 1855, pp. 154–169. Springer (2000)
  * [28] Cousineau, D.: Fitting the three-parameter Weibull distribution: review and evaluation of existing and new methods. IEEE DEIS 16(1), 281–288 (2009)
  * [29] Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Synthesis in pMDPs: A tale of 1001 parameters. In: ATVA. LNCS, vol. 11138, pp. 160–176. Springer (2018)
  * [30] Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Convex optimization for parameter synthesis in MDPs. IEEE Trans. Aut. Contr. (2022)
  * [31] Cubuktepe, M., Jansen, N., Junges, S., Marandi, A., Suilen, M., Topcu, U.: Robust finite-state controllers for uncertain POMDPs. In: AAAI. pp. 11792–11800. AAAI Press (2021)
  * [32] Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: ICTAC. LNCS, vol. 3407, pp. 280–294. Springer (2004)
  * [33] Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.P., Ábrahám, E.: Prophesy: A probabilistic parameter synthesis tool. In: CAV. LNCS, vol. 9206, pp. 214–231. Springer (2015)
  * [34] Esparza, J., Hoffmann, P., Saha, R.: Polynomial analysis algorithms for free choice probabilistic workflow nets. Perform. Evaluation 117, 104–129 (2017)
  * [35] Fang, X., Calinescu, R., Gerasimou, S., Alhwikem, F.: Fast parametric model checking through model fragmentation. In: ICSE. pp. 835–846. IEEE (2021)
  * [36] Filieri, A., Tamburrelli, G., Ghezzi, C.: Supporting self-adaptation via quantitative verification and sensitivity analysis at run time. IEEE Trans. Software Eng. 42(1), 75–99 (2016)
  * [37] Gainer, P., Hahn, E.M., Schewe, S.: Accelerated model checking of parametric Markov chains. In: ATVA. LNCS, vol. 11138, pp. 300–316. Springer (2018)
  * [38] Givan, R., Leach, S.M., Dean, T.L.: Bounded-parameter Markov decision processes. Artif. Intell. 122(1-2), 71–109 (2000)
  * [39] Gouberman, A., Siegle, M., Tati, B.: Markov chains with perturbed rates to absorption: Theory and application to model repair. Perform. Evaluation 130, 32–50 (2019)
  * [40] Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. STTT 13(1), 3–19 (2010)
  * [41] Hajnal, M., Nouvian, M., Petrov, T., Safránek, D.: Data-informed parameter synthesis for population Markov chains. In: CMSB. LNCS, vol. 11773, pp. 383–386. Springer (2019)
  * [42] Han, Y.: State elimination heuristics for short regular expressions. Fundam. Inform. 128(4), 445–462 (2013)
  * [43] Hartmanns, A., Katoen, J.P., Kohlen, B., Spel, J.: Tweaking the odds in probabilistic timed automata. In: QEST. LNCS, vol. 12846, pp. 39–58. Springer (2021)
  * [44] Haselman, M., Hauck, S.: The future of integrated circuits: A survey of nanoelectronics. Proc. of the IEEE 98(1), 11–38 (2010)
  * [45] Herman, T.: Probabilistic self-stabilization. Inf. Process. Lett. 35(2), 63–67 (1990)
  * [46] Holtzen, S., Junges, S., Vazquez-Chanlatte, M., Millstein, T.D., Seshia, S.A., Van den Broeck, G.: Model checking finite-horizon Markov chains with probabilistic inference. In: CAV (2). LNCS, vol. 12760, pp. 577–601. Springer (2021)
  * [47] Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley (2003)
  * [48] Hutschenreiter, L., Baier, C., Klein, J.: Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. In: GandALF. EPTCS, vol. 256, pp. 16–30 (2017)
  * [49] Jansen, N., Corzilius, F., Volk, M., Wimmer, R., Ábrahám, E., Katoen, J.P., Becker, B.: Accelerating parametric probabilistic verification. In: QEST. LNCS, vol. 8657, pp. 404–420. Springer (2014)
  * [50] Junges, S.: Parameter Synthesis in Markov Models. Dissertation, RWTH Aachen University (2020)
  * [51] Junges, S., Ábrahám, E., Hensel, C., Jansen, N., Katoen, J.P., Quatmann, T., Volk, M.: Parameter synthesis for Markov models. CoRR abs/1903.07993 (2019)
  * [52] Junges, S., Jansen, N., Wimmer, R., Quatmann, T., Winterer, L., Katoen, J.P., Becker, B.: Finite-state controllers of POMDPs using parameter synthesis. In: UAI. pp. 519–529. AUAI Press (2018)
  * [53] Junges, S., Katoen, J.P., Pérez, G.A., Winkler, T.: The complexity of reachability in parametric Markov decision processes. J. Comput. Syst. Sci. 119, 183–210 (2021)
  * [54] Junges, S., Spaan, M.T.J.: Abstraction-refinement for hierarchical probabilistic models. In: CAV (2022), to appear
  * [55] Katoen, J.P.: The probabilistic model checking landscape. In: LICS. pp. 31–45. ACM (2016)
  * [56] Knuth, D., Yao, A.: Algorithms and Complexity: New Directions and Recent Results, chap. The complexity of nonuniform random number generation. Academic Press (1976)
  * [57] Kochenderfer, M.J.: Decision Making Under Uncertainty: Theory and Application. MIT Press (2015)
  * [58] Kozine, I., Utkin, L.V.: Interval-valued finite Markov chains. Reliab. Comput. 8(2), 97–113 (2002)
  * [59] Krak, T.E., T’Joens, N., Bock, J.D.: Hitting times and probabilities for imprecise Markov chains. In: ISIPTA. PMLR, vol. 103, pp. 265–275. PMLR (2019)
  * [60] Kwiatkowska, M., Norman, G., Parker, D.: Prism 4.0: Verification of probabilistic real-time systems. In: CAV. LNCS, vol. 6806, pp. 585–591. Springer (2011)
  * [61] Madani, O., Hanks, S., Condon, A.: On the undecidability of probabilistic planning and related stochastic optimization problems. Artif. Intell. 147(1-2), 5–34 (2003)
  * [62] Mao, Y., Szmuk, M., Xu, X., Acikmese, B.: Successive Convexification: A Superlinearly Convergent Algorithm for Non-convex Optimal Control Problems. arXiv preprint arXiv:1804.06539 (2018)
  * [63] Nilim, A., El Ghaoui, L.: Robust Control of Markov Decision Processes with Uncertain Transition Matrices. Operations Research 53(5), 780–798 (2005)
  * [64] Pathak, S., Ábrahám, E., Jansen, N., Tacchella, A., Katoen, J.P.: A greedy approach for the efficient repair of stochastic models. In: NFM. LNCS, vol. 9058, pp. 295–309. Springer (2015)
  * [65] Peruffo, A., Abate, A.: Formal abstraction and synthesis of parametric stochastic processes. In: FORMATS. LNCS, vol. 12860, pp. 135–153. Springer (2021)
  * [66] Polgreen, E., Wijesuriya, V.B., Haesaert, S., Abate, A.: Automated experiment design for data-efficient verification of parametric Markov decision processes. In: QEST. LNCS, vol. 10503, pp. 259–274. Springer (2017)
  * [67] Poupart, P., Boutilier, C.: Bounded finite state controllers. In: NIPS. pp. 823–830. MIT Press (2003)
  * [68] Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: CAV. LNCS, vol. 8044, pp. 527–542. Springer (2013)
  * [69] Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons (1994)
  * [70] Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.P.: Parameter synthesis for Markov models: Faster than ever. In: ATVA. LNCS, vol. 9938, pp. 50–67 (2016)
  * [71] Russell, S.J., Norvig, P.: Artificial Intelligence - A Modern Approach (3. internat. ed.). Pearson Education (2010)
  * [72] Salmani, B., Katoen, J.P.: Fine-tuning the odds in Bayesian networks. In: ECSQARU. LNCS, vol. 12897, pp. 268–283. Springer (2021)
  * [73] Salmani, B., Katoen, J.P.: Automatically finding the right probabilities in Bayesian networks. arXiv preprint arXiv: (2022), to appear
  * [74] Skulj, D.: Discrete time Markov chains with interval probabilities. Int. J. Approx. Reason. 50(8), 1314–1329 (2009)
  * [75] Spaan, M.T.J.: Partially observable Markov decision processes. In: Reinforcement Learning, Adaptation, Learning, and Optimization, vol. 12, pp. 387–414. Springer (2012)
  * [76] Spel, J., Heck, L., Junges, S., Moerman, J., Katoen, J.P.: Gradient-descent for randomized controllers under partial observability. In: VMCAI. LNCS, vol. 13182, pp. 127–150. Springer (2022)
  * [77] Spel, J., Junges, S., Katoen, J.P.: Are parametric Markov chains monotonic? In: ATVA. LNCS, vol. 11781, pp. 479–496. Springer (2019)
  * [78] Spel, J., Junges, S., Katoen, J.P.: Finding provably optimal Markov chains. In: TACAS (1). LNCS, vol. 12651, pp. 173–190. Springer (2021)
  * [79] Suilen, M., Jansen, N., Cubuktepe, M., Topcu, U.: Robust policy synthesis for uncertain POMDPs via convex optimization. In: IJCAI. pp. 4113–4120. ijcai.org (2020)
  * [80] Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS. pp. 327–338. IEEE Computer Society (1985)
  * [81] Vlassis, N., Littman, M.L., Barber, D.: On the computational complexity of stochastic controller optimization in POMDPs. ACM Trans. Comput. Theory 4(4), 12:1–12:8 (2012)
  * [82] Volk, M., Bonakdarpour, B., Katoen, J.P., Aflaki, S.: Synthesizing optimal bias in randomized self-stabilization. Distributed Comput. 35(1), 37–57 (2022)
  * [83] Wiesemann, W., Kuhn, D., Rustem, B.: Robust Markov decision processes. Mathematics of Operations Research 38(1), 153–183 (2013)
  * [84] Wolff, E.M., Topcu, U., Murray, R.M.: Robust control of uncertain Markov decision processes with temporal logic specifications. In: CDC. pp. 3372–3379. IEEE (2012)
  * [85] Yuan, Y.X.: Recent advances in trust region algorithms. Math. Program. 151(1), 249–281 (2015)