From 90459e1f7488f39e97f1a014d958b5445746daf3 Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Thu, 5 Jul 2018 12:54:09 +0200
Subject: Explain difference probabilistic and cost-bounded properties

---
 Assignment2/report/intro.tex | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'Assignment2/report/intro.tex')

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
-- 
cgit v1.2.3


From dad7be659309a95befa28219c00b6fc2e046f7cf Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Thu, 5 Jul 2018 13:02:36 +0200
Subject: Remove duplicate PCTL

---
 Assignment2/report/intro.tex | 13 ++-----------
 1 file changed, 2 insertions(+), 11 deletions(-)

(limited to 'Assignment2/report/intro.tex')

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:
-- 
cgit v1.2.3

