diff options
Diffstat (limited to 'Assignment2/report/intro.tex')
| -rw-r--r-- | Assignment2/report/intro.tex | 14 |
1 files changed, 13 insertions, 1 deletions
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 |