Lalala

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$.