Remove duplicate PCTL

1 files changed, 2 insertions, 11 deletions

diff --git a/Assignment2/report/intro.tex b/Assignment2/report/intro.tex
index 2d1bd5f..540a9ae 100644
--- a/Assignment2/report/intro.tex
+++ b/Assignment2/report/intro.tex
@@ -14,17 +14,8 @@ 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$.
+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 first approach to automatically perform Model Repair was introduced by Bartocci et al. \cite[327]{Bartocci2011}.
 Additionally, they define the Model Repair problem as: