Finish Summary

1 files changed, 24 insertions, 3 deletions

diff --git a/PCTL/pctl.tex b/PCTL/pctl.tex
index ad58267..0aac80d 100644
--- a/PCTL/pctl.tex
+++ b/PCTL/pctl.tex
@@ -35,7 +35,7 @@
 			\enspace\middle|\enspace a
 			\enspace\middle|\enspace \Phi_1 \land \Phi_2
 			\enspace\middle|\enspace \lnot \Phi
-			\enspace\middle|\enspace \mathbb{P}_J(\phi)
+			\enspace\middle|\enspace \mathbb{P}_J(\Psi)
 			\right.
 	\]
 	where $a \in AP$, $\phi$ is a path formula and $J \subseteq [0,1]$ is an interval with rational bounds.
@@ -45,9 +45,9 @@
 \begin{definition}[Syntax of PCTL Path Formulas]
 	PCTL Path formulas are formed according to the following grammar:
 	\[
-		\Phi
+		\Psi
 			::=
-			\left.\raisebox{0pt}[5pt][5pt]{} \Xop\Phi
+			\left.\raisebox{0pt}[5pt][5pt]{} \Xop\Psi
 			\enspace\middle|\enspace \Phi_1 \Uop \Phi_2
 			\enspace\middle|\enspace \Phi_1 \Uop^{\leq n} \Phi_2
 			\right.
@@ -76,4 +76,25 @@ As mentioned above, PCTL can be seen as quantitative analogues of the $\forall$
 	\item $\mathbb{P}_{>0}(\Fop\phi) \Leftrightarrow \exists\Fop\phi$
 	\item $\mathbb{P}_1(\Fop\phi)$ is weaker than $\forall\Fop\phi$
 \end{itemize}
+
+\section{Model Checking}
+Model Checking is done in the same way as with CTL modelchecking.
+The difference lies with the fact that probabilities must now be taken into account.
+\[
+	Sat(\mathbb{P}_J(\phi)) = \{s \in S \mid P(s \vDash \phi) \in J \}
+\]
+
+\section{PCTL*}
+A subsumption of LTL and PCTL that modifies the path formulas to be the following:
+\[
+	\Psi
+		::=
+		\left.\raisebox{0pt}[5pt][5pt]{} \Phi
+		\enspace\middle|\enspace \Psi_1 \land \Psi_2
+		\enspace\middle|\enspace \neg\Psi
+		\enspace\middle|\enspace \Xop\Psi
+		\enspace\middle|\enspace \Psi_1 \Uop \Psi_2
+		\right.
+\]
+The state formulas are not modified.
 \end{document}