1 files changed, 79 insertions, 0 deletions
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}