From 3ce91bf844723be99e183bee375bf447d9f9b237 Mon Sep 17 00:00:00 2001 From: Erin van der Veen Date: Mon, 23 Apr 2018 21:20:53 +0200 Subject: Mention that the translation Muller -> LTL lies outside the scope of this book. --- Assignment1/conversion.tex | 5 +++-- 1 file changed, 3 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 -- cgit v1.2.3 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 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(-) 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