From a7cea2181b5cb75e2ff62ad5a80c9532880e5346 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Fri, 6 Jul 2018 21:37:11 +0200
Subject: Lalala

---
 Assignment2/report/intro.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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

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

