\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}