1 files changed, 25 insertions, 0 deletions
diff --git a/Assignment2/report/intro.tex b/Assignment2/report/intro.tex
new file mode 100644
index 0000000..db0469f
--- /dev/null
+++ b/Assignment2/report/intro.tex
@@ -0,0 +1,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.