From cf5e509c546886bd2587541b0df2f085410a7b27 Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Tue, 8 May 2018 10:48:14 +0200
Subject: Start pctl summary

---
 PCTL/pctl.tex | 79 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 79 insertions(+)
 create mode 100644 PCTL/pctl.tex

(limited to 'PCTL/pctl.tex')

diff --git a/PCTL/pctl.tex b/PCTL/pctl.tex
new file mode 100644
index 0000000..ad58267
--- /dev/null
+++ b/PCTL/pctl.tex
@@ -0,0 +1,79 @@
+\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(\phi)
+			\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:
+	\[
+		\Phi
+			::=
+			\left.\raisebox{0pt}[5pt][5pt]{} \Xop\Phi
+			\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}
+\end{document}
-- 
cgit v1.2.3


From cc5e7080148485896a61024d172ce6234205cc68 Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Mon, 14 May 2018 17:37:25 +0200
Subject: Finish Summary

---
 PCTL/pctl.tex | 27 ++++++++++++++++++++++++---
 1 file changed, 24 insertions(+), 3 deletions(-)

(limited to 'PCTL/pctl.tex')

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

