Explain difference probabilistic and cost-bounded properties

2 files changed, 15 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..2d1bd5f 100644
--- a/Assignment2/report/intro.tex
+++ b/Assignment2/report/intro.tex
@@ -14,8 +14,20 @@ 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$.
 
+A distinction between two kinds of properties is made.
+A probabilistic reachability property $\phi$ is a property of the form:
+\[
+	\phi = \mathbb{P}_{J}(\phi')
+\]
+where $\phi'$ is a PCTL formula, $J \subseteq [0,1]$ and $\mathbb{P}$ is a function that determines if the probability of satisfying $\phi'$ is in $J$.
+A expected cost property $\phi$ is a property of the form:
+\[
+	\phi = \mathbb{E}_R(\phi')
+\]
+where $\phi'$ is a PRCTL formula, $R$ are intervals with rational bounds, and $\mathbb{E}$ is 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