blob: 0aac80dfb955c1e2f4882b1ea168fa1535f534d5 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
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}
|
