Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking

2 files changed, 103 insertions, 2 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index fe9b136..be5196f 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -446,14 +446,15 @@ This theorem, in combination with the work of \citet{Meyer1969}, allows for the
 	\begin{enumerate}
 		\item Each $B_i$ is a permutation-reset automaton\footnote{\label{note:definition-omitted}Definition omitted for brevity.}
 		\item There is a homomorphism\footnote{See \cref{note:definition-omitted}.} $\phi$ from $C$ to $A$
-		\item Any permutation in some $B_i$ is homomorphic to a subgroup of the tranformation semigroup of $A$
+		\item Any permutation in some $B_i$ is homomorphic to a subgroup of the transformation semigroup of $A$
 	\end{enumerate}
 \end{theorem}
 
 The cascade product can then be used to create star-free regular sets.
 These sets can then be transformed into LTL formulae.
+We will not discuss this transformation in detail since it lies beyond the scope of this book.
 
 \cbend
 %Provide the syntactic algorithm to convert PLTL to LTL
-%TODO: Provide algorithm via automata to convert PLTL to LTL
+%Provide algorithm via automata to convert PLTL to LTL
 %TODO: In both cases make use of examples from SSH Paper
diff --git a/PCTL/pctl.tex b/PCTL/pctl.tex
new file mode 100644
index 0000000..0aac80d
--- /dev/null
+++ b/PCTL/pctl.tex
@@ -0,0 +1,100 @@
+\documentclass[a4paper]{scrartcl}
+
+\usepackage{amsmath}
+\usepackage{amsthm}
+\usepackage{amssymb}
+\usepackage{mathtools}
+
+\newtheorem{theorem}{Theorem}
+\newtheorem{definition}{Definition}
+
+\DeclareMathOperator{\defeq}{\overset{\text{def}}{=}}
+\DeclareMathOperator{\Uop}{\mathbf{U}}
+\DeclareMathOperator{\Wop}{\mathbf{W}}
+\DeclareMathOperator{\Xop}{\raisebox{1pt}{$\bigcirc$}}
+\DeclareMathOperator{\Fop}{\lozenge}
+\DeclareMathOperator{\Gop}{\square}
+\DeclareMathOperator{\Sop}{\mathbf{S}}
+\DeclareMathOperator{\Pop}{\raisebox{1pt}{$\bigcirc$}^{--1}}
+
+\title{PCTL}
+\subtitle{A Summary of 10.2 and 10.6.2}
+\author{Erin van der Veen}
+
+\begin{document}
+
+\maketitle
+
+\section{Syntax}
+\begin{definition}[Syntax of PCTL State Formulas]
+	PCTL state formulas over the set $AP$ of atomic propositions are formed according to the following grammar:
+	\[
+		\Phi
+			::=
+			\left.\raisebox{0pt}[5pt][5pt]{} \text{true}
+			\enspace\middle|\enspace a
+			\enspace\middle|\enspace \Phi_1 \land \Phi_2
+			\enspace\middle|\enspace \lnot \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.
+	Where $\mathbb{P}_J(\phi)$ in state $s$ means that the probability for the set of paths satisfying $\phi$ and starting in $s$ meets the bounds given by $J$.
+\end{definition}
+
+\begin{definition}[Syntax of PCTL Path Formulas]
+	PCTL Path formulas are formed according to the following grammar:
+	\[
+		\Psi
+			::=
+			\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.
+	\]
+\end{definition}
+
+PCTL does not incorporate the existential and universal quantifiers that are present in CTL.
+Reasoning for this difference is that the $P$-operator can be used to closely mimic\footnote{Consider, for example, an infinite path whose probability is 0} the behavior of these operators.
+
+\section{Semantics}
+\begin{definition}[Semantics of PCTL]
+	\[
+		\begin{matrix*}[l]
+			s \vDash & a                  &\text{iff} & a \in L(s)\\
+			s \vDash & \lnot\phi          &\text{iff} & s \nvDash \phi\\
+			s \vDash & \phi \land \psi    &\text{iff} & \text{$s \vDash \phi$ and $ s \vDash \psi$}\\
+			s \vDash & \mathbb{P}_J(\phi) &\text{iff} & Pr(s \vDash \phi) \in J\\
+		\end{matrix*}
+	\]
+\end{definition}
+
+As mentioned above, PCTL can be seen as quantitative analogues of the $\forall$ and $\exists$ operators of CTL.
+\begin{itemize}
+	\item Qualitative PCTL properties are those where $J$ in $\mathbb{P}_J(\phi)$ is 1 or 0.
+	\item Quantitative PCTL properties are those where $J$ in $\mathbb{P}_J(\phi)$ is in the range $(0,1)$
+	\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}