Continue introduction

3 files changed, 99 insertions, 6 deletions

diff --git a/Assignment2/report/assignment2.tex b/Assignment2/report/assignment2.tex
index 20f7ceb..f8edcaf 100644
--- a/Assignment2/report/assignment2.tex
+++ b/Assignment2/report/assignment2.tex
@@ -2,6 +2,10 @@
 
 \usepackage{amsmath}
 \usepackage{amssymb}
+\usepackage{cleveref}
+\usepackage{csquotes}
+\usepackage{tikz}
+\usetikzlibrary{automata,positioning}
 
 \let\leq\leqslant
 \let\le\leqslant
diff --git a/Assignment2/report/intro.tex b/Assignment2/report/intro.tex
index 540a9ae..7e41932 100644
--- a/Assignment2/report/intro.tex
+++ b/Assignment2/report/intro.tex
@@ -7,22 +7,85 @@ The transition probability function and the initial distribution should be total
 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.
+A scheduler $\sigma$ on an MDP $\mathcal M$ induces the DTMC $\mathcal M^\sigma$ by choosing an action in each state,
+	given the path fragment leading up to that state~\cite[842]{BK}.
 
 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 semantics are that $\Phi_2$ should be satisfied at most $n$ steps after $\Phi_1$.%
+	\footnote{%
+		Furthermore, to PCTL adds state formulae $\mathbb E_R(\phi)$ to accommodate Markov Reward Models (a Markov Chain with a reward function mapping states or transitions to natural numbers~\cite[817]{BK}).
+		Here, $R$ is an interval with rational bounds, $\phi$ a path formula, and $\mathbb{E}$ a function that determines the cost of satisfying $\phi$ in $R$.
+		Since $\mathbb E$ is not relevant to the present discussion, we do not discuss it in further detail.}
 
-For Markov Reward Models (MRMs) PCTL is not enough, as it cannot express satisfiability of costs.
-For this, it adds state formula $\mathbb E_R(\phi)$, where $R$ is an interval with rational bounds, $\phi$ a path formula, and $\mathbb{E}$ a function that determines is the cost of satisfying $\phi$ is in $R$.
+The Model Checking problem for a PCTL state formula $\Phi$ and a state $s$ in a DTMC is to verify whether $s \vDash \Phi$.
+Model checking proceeds as for the plain CTL case, by computing the satisfaction set of the subformulas of $\Phi$.
+The satisfaction set of $\mathbb P_J(\phi)$ can be computed using a linear equation system~\cite[785]{BK}.
+An MDP satisfies a formula if the formula is satisfied by the induced DTMCs of all possible schedulers.
+Model checking of MDPs is possible since there exist finite-memory schedulers optimising reachability properties~\cite[865--866]{BK}.
 
-The first approach to automatically perform Model Repair was introduced by Bartocci et al. \cite[327]{Bartocci2011}.
-Additionally, they define the Model Repair problem as:
+However, for complex systems, the answer to the Model Checking problem (\enquote{yes} or \enquote{no} with a counterexample) is little helpful,
+	as it may not be clear at all how the model should be changed to make it satisfy the property.
+For this purpose, we define the Model Repair problem as 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,
+Furthermore, we may score reparations using a \emph{cost} function,
 	and want a Model Repair tool to minimise this cost.
+
+A straightforward cost function is the mean squared error (MSE).
+For all pairs of states $s_1,s_2$ in the original model $M$,
+	we compute the squared error as the square of the difference of the probabilities of $s_1\to s_2$ in $M$ and the repaired model $M'$.
+The MSE is the average of these individual error measures.
+It does not distinguish between different transitions, but by squaring it prefers multiple minor modifications over one major modification.
+The MSE is well-established in statistics.
+Of course, in the usual case where we only need to consider one model with different reparations,
+	the size of $M$ is fixed and we may use the sum of squared errors (SSE) as well.
+
+Another reasonable cost function is the number of modified transitions.
+This measure counts the pairs of states $s_1,s_2$ for which the probability of $s_1\to s_2$ differs between $M$ and $M'$.
+The intuition is that the model is almost correct but may contain human errors, such as off-by-one errors or typos.
+
+\begin{figure}
+	\centering
+	\begin{tikzpicture}[->,>=stealth,scale=0.9,every node/.style={scale=0.9,transform shape}]
+		\node[state,initial,initial text={}] (s0) {$s_0$};
+
+		\node[state,above right=of s0] (s1) {$s_1$};
+		\draw (s0) -- node[above left] {$p$} ++ (s1);
+		\node[state,above right=of s1] (s3) {$s_3$};
+		\draw (s1) -- node[below right] {$p$} ++ (s3);
+		\draw (s3) edge[bend right=45] node[above left] {$p$} (s1);
+		\node[state,right=of s3,label={right:\enquote{1}}] (s7) {$s_7$};
+		\draw (s3) -- node[above] {$1-p$} ++ (s7);
+		\node[state,below right=of s1,yshift=3em] (s4) {$s_4$};
+		\draw (s1) -- node[below,xshift=-.5em] {$1-p$} ++ (s4);
+		\node[state,right=of s4,yshift=2.7em,label={right:\enquote{2}}] (s8) {$s_8$};
+		\draw (s4) -- node[above] {$p$} ++ (s8);
+		\node[state,right=of s4,yshift=-1em,label={right:\enquote{3}}] (s9) {$s_9$};
+		\draw (s4) -- node[below] {$1-p$} ++ (s9);
+
+		\node[state,below right=of s0] (s2) {$s_2$};
+		\draw (s0) -- node[below left] {$1-p$} ++ (s2);
+		\node[state,above right=of s2,yshift=-3em] (s5) {$s_5$};
+		\draw (s2) -- node[above,xshift=-.5em] {$1-p$} ++ (s5);
+		\node[state,right=of s5,yshift=1em,label={right:\enquote{4}}] (s10) {$s_{10}$};
+		\draw (s5) -- node[above] {$p$} ++ (s10);
+		\node[state,right=of s5,yshift=-2.7em,label={right:\enquote{5}}] (s11) {$s_{11}$};
+		\draw (s5) -- node[below] {$1-p$} ++ (s11);
+		\node[state,below right=of s2] (s6) {$s_6$};
+		\draw (s2) -- node[above right] {$p$} ++ (s6);
+		\draw (s6) edge[bend left=45] node[below left] {$p$} (s2);
+		\node[state,right=of s6,label={right:\enquote{6}}] (s12) {$s_{12}$};
+		\draw (s6) -- node[above] {$1-p$} ++ (s12);
+	\end{tikzpicture}
+	\caption{The Knuth-Yao die model~\cite{KnuthYao1976}.\label{fig:knuth-yao}}
+\end{figure}
+
+The present paper discusses a straightforward method to build a Model Repair pipeline using a Model Checking tool and an SMT solver.
+The authors' implementation uses Storm~\cite{Storm} and Z3~\cite{Z3}, but the technique is agnostic as to what tool is used.
+As a running example, we will be using the well-known Knuth-Yao die~\cite{KnuthYao1976}, using a potentially unfair coin (see \cref{fig:knuth-yao}).
diff --git a/Assignment2/report/library.bib b/Assignment2/report/library.bib
index dab46d6..db8f78c 100644
--- a/Assignment2/report/library.bib
+++ b/Assignment2/report/library.bib
@@ -26,3 +26,29 @@
 	publisher={Academic Press},
 	year=1976
 }
+
+@inproceedings{Storm,
+	title={A Storm is Coming: A Modern Probabilistic Model Checker},
+	author={Dehnert, Christian and Junges, Sebastian and Katoen, Joost-Pieter and Volk, Matthias},
+	booktitle={Computer Aided Verification. CAV 2017},
+	editor={Majumdar, R. and Kun\v{c}ak, V.},
+	pages={592--600},
+	series={Lecture Notes in Computer Science},
+	number=10427,
+	publisher={Springer},
+	address={Cham},
+	year=2017
+}
+
+@inproceedings{Z3,
+	title={Z3: An Efficient SMT Solver},
+	author={{de Moura}, Leonardo and Bj{\o}rner, Nikolaj},
+	booktitle={Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2008},
+	editor={Ramakrishnan, C. R. and Rehof, J.},
+	pages={337--340},
+	series={Lecture Notes in Computer Science},
+	number=4963,
+	publisher={Springer},
+	address={Berlin, Heidelberg},
+	year=2008
+}