diff options
Diffstat (limited to 'Assignment2/report/intro.tex')
| -rw-r--r-- | Assignment2/report/intro.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Assignment2/report/intro.tex b/Assignment2/report/intro.tex index 9d9121c..90f8ff7 100644 --- a/Assignment2/report/intro.tex +++ b/Assignment2/report/intro.tex @@ -14,11 +14,11 @@ Properties of DTMCs and MDPs are typically described using Probabilistic Computa It adds state formulae $\mathbb P_J(\phi)$, where $J$ is an interval with rational bounds and $\phi$ a path formula. A state $s$ satisfies $\mathbb P_J(\phi)$ iff the probability of satisfying $\phi$ for a path starting in $s$ is in $J$. 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$.% + the semantics are that $\Phi_2$ should be satisfied at most $n$ steps after $\Phi_1$% \footnote{% - Furthermore, to PCTL adds state formulae $\mathbb E_R(\phi)$ to accommodate Markov Reward Models (a Markov Chain with a reward function mapping states or transitions to natural numbers~\cite[817]{BK}). + Furthermore, PCTL adds state formulae $\mathbb E_R(\phi)$ to accommodate Markov Reward Models (a Markov Chain with a reward function mapping states or transitions to natural numbers~\cite[817]{BK}). Here, $R$ is an interval with rational bounds, $\phi$ a path formula, and $\mathbb{E}$ a function that determines the cost of satisfying $\phi$ in $R$. - Since $\mathbb E$ is not relevant to the present discussion, we do not discuss it in further detail.} + Since $\mathbb E$ is not relevant to the present discussion, we do not discuss it in further detail.}. The Model Checking problem for a PCTL state formula $\Phi$ and a state $s$ in a DTMC is to verify whether $s \vDash \Phi$. Model checking proceeds as for the plain CTL case, by computing the satisfaction set of the subformulas of $\Phi$. |