Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking

2 files changed, 6 insertions, 1 deletions

diff --git a/Assignment2/report/assignment2.tex b/Assignment2/report/assignment2.tex
index 29ec95a..20f7ceb 100644
--- a/Assignment2/report/assignment2.tex
+++ b/Assignment2/report/assignment2.tex
@@ -10,6 +10,8 @@
 
 \DeclareMathOperator{\Uop}{\mathsf{U}}
 
+\newcommand{\PRISM}{\texttt{PRISM}}
+
 \begin{document}
 
 \title{Model Repair in Practice}
diff --git a/Assignment2/report/intro.tex b/Assignment2/report/intro.tex
index db0469f..540a9ae 100644
--- a/Assignment2/report/intro.tex
+++ b/Assignment2/report/intro.tex
@@ -14,8 +14,11 @@ A state $s$ satisfies $\mathbb P_J(\phi)$ iff the probability of satisfying $\ph
 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$.
 
+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 Repair problem was first introduced by Bartocci et al. \cite[327]{Bartocci2011}:
+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:
 \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