1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
\section{Introduction}
A Discrete-Time Markov Chain (DTMC) is a Kripke structure enhanced with a \emph{transition probability function} $P : S\times S\to [0,1]$,
indicating the probability of moving from one state to another state,
and an \emph{initial distribution} $\iota_{\text{init}} : S\to [0,1]$,
indicating for each state the probability of starting in it~\cite[747--748]{BK}.
The transition probability function and the initial distribution should be total, i.e., the probabilities (per state) sum up to one.
A Markov Decision Process (MDP) further extends a DTMC with nondeterministic choice.
It adds a set of actions $\textsl{Act}$ and uses $P : S\times \textsl{Act}\times S\to [0,1]$ as the transition probability function~\cite[833--834]{BK}.
The transition probability function should still be total for pairs of states and actions.
Properties of DTMCs and MDPs are typically described using Probabilistic Computation Tree Logic (PCTL), an extension of CTL~\cite[780--781]{BK}.
It adds state formulae $\mathbb P_J(\phi)$, where $J$ is an interval with rational bounds and $\phi$ a path formula.
A state $s$ satisfies $\mathbb P_J(\phi)$ iff the probability of satisfying $\phi$ for a path starting in $s$ is in $J$.
PCTL also adds the bounded-until path formula $\Phi_1 \Uop^{\le n} \Phi_2$, where $n\in \mathbb N$ and $\Phi_{1,2}$ are state formulae ---
the semantics are that $\Phi_2$ should be satisfied at most $n$ steps after $\Phi_1$.
The Model Repair problem was first introduced by Bartocci et al. \cite[327]{Bartocci2011}:
\begin{quote}
Given a probabilistic system $M$ and a probabilistic temporal logic formula $\phi$ such that $M$ fails to satisfy $\phi$,
the \emph{probabilistic Model Repair problem} is to find an $M'$ that
satisfies $\phi$ and differs from $M$ only in the transition flows of those states in $M$ that are deemed \emph{controllable}.
\end{quote}
Furthermore, we may score the reparation using a \emph{cost} function,
and want a Model Repair tool to minimise this cost.
|
