diff options
Diffstat (limited to 'Assignment1')
| -rw-r--r-- | Assignment1/assignment1.tex | 1 | ||||
| -rw-r--r-- | Assignment1/conversion.tex | 5 | ||||
| -rw-r--r-- | Assignment1/intro.tex | 3 | ||||
| -rw-r--r-- | Assignment1/specifying-properties.tex | 13 | ||||
| -rw-r--r-- | Assignment1/syntax.tex | 30 |
5 files changed, 27 insertions, 25 deletions
diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex index 1e5a55a..e8e34dd 100644 --- a/Assignment1/assignment1.tex +++ b/Assignment1/assignment1.tex @@ -111,7 +111,6 @@ \input{intro} \input{syntax} \input{semantics} -\input{specifying-properties} \input{equivalence} \input{conversion} %TODO: (Section?) Assess if PLTL is actually more succinct using the examples from the SSH Paper diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex index 72304d2..3f4cf0f 100644 --- a/Assignment1/conversion.tex +++ b/Assignment1/conversion.tex @@ -7,6 +7,7 @@ The second algorithm makes use of the translation of PLTL formulas to automata a This algorithm is described in more detail below. \paragraph{Syntactic Algorithm} +\label{pltl:to-ltl:syntactic} The syntactic algorithm as proposed by Gabbay has its foundation in the following three facts:% \footnote{% Note that Gabbay used a slightly different, \enquote{non-strict} definition for the $\Uop$ and $\Sop$ operators. @@ -144,7 +145,7 @@ These equivalences also hold when the path is reversed, so similar elimination r The final step of the algorithm entails removing the parts of the formula that contains the $\Sop$-operators. \camil -\begin{example}[Properties for an Authentication System] +\begin{example}[A property for an Authentication System] \label{ex:pltl-to-ltl:authentication} Consider again the property from \cref{ex:pltl:authentication-system}, repeated here with less verbose names: $\phi = \square (c \rightarrow \lnot f \Sop s)$. @@ -338,8 +339,8 @@ Let us first define the Muller Automaton: Converting a NBA to a Muller automaton was shown to be possible by R. McNaughton~\cite{McNaughton1966} and is part of what is known as McNaughton's theorem. - \cbend + %Provide the syntactic algorithm to convert PLTL to LTL %TODO: Provide algorithm via automata to convert PLTL to LTL %TODO: In both cases make use of examples from SSH Paper diff --git a/Assignment1/intro.tex b/Assignment1/intro.tex index d07be86..15294ee 100644 --- a/Assignment1/intro.tex +++ b/Assignment1/intro.tex @@ -17,7 +17,8 @@ Eventually, formal computing scientists stopped using past modalities for reason In 2003, Nicolas Markey showed that while past modalities do not increase expressive power, they can make LTL formulas exponentially more succinct~\cite{Markey2003}. In other words, there is a class of PLTL formulae% - \footnote{In keeping with the style of the rest of the book, we alternate between \enquote{formulas} and \enquote{formulae} and wish the reader best of luck with this.} + \footnote{In keeping with the style of the rest of the book, we alternate between \enquote{formulas} and \enquote{formulae} and wish the reader best of luck with this. + (Like the book, this section may contain typos and inaccuracies. These are however not intentional.)} for which the size of all equivalent LTL formulas is $\Omega\left(2^n\right)$. Markey achieves this proof by providing a formula that is in exactly this class. Besides being smaller, PLTL formulas can also be easier to write and understand, as examples below will demonstrate. diff --git a/Assignment1/specifying-properties.tex b/Assignment1/specifying-properties.tex deleted file mode 100644 index 0f84a4e..0000000 --- a/Assignment1/specifying-properties.tex +++ /dev/null @@ -1,13 +0,0 @@ -\subsubsection{Specifying Properties} -% TODO Once operator - -\camil -\begin{remark}[Other Notations] - % TODO: I don't find this place logical for this remark, but it is the same place as Remark 5.16 in the book. - Like for LTL, many different notations are used in literature for PLTL. - These include - $\mathbf X^{-1}, \mathbf G^{-1}, \mathbf F^{-1}$~\citep[e.g.]{Markey2003}, - but also \raisebox{-1pt}{\tikz\draw[black,fill=black](0,0)circle(.4em);}$,\blacksquare,\blacklozenge$~\citep[e.g.]{Gabbay1989} - or $\stackinset{c}{}{c}{}{$\cdot$}{$\bigcirc$},\boxdot,\stackinset{c}{}{c}{}{$\cdot$}{$\lozenge$}$~\citep[e.g.]{Havelund2002}. - % It is always fun to come up with new versions and watch people struggling to reproduce them in \LaTeX. -\end{remark} diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex index 8543669..708d3b8 100644 --- a/Assignment1/syntax.tex +++ b/Assignment1/syntax.tex @@ -61,6 +61,7 @@ In discourse, it can be helpful to distinguish different kinds of PLTL formulas. Note that the classes \wffn, \wffp\ and \wfff\ are mutually disjoint. Furthermore, there are \wff\ which are neither, like $\Xop a \land \Xop^{-1} a$. +However, as we will see in \cref{pltl:to-ltl:syntactic}, every PLTL formula can be written as a boolean combination of $\wfff \cup \wffp \cup \wffn$. As with LTL, we can also derive additional operators in PLTL. They can be seen as counterparts of the derived LTL modalities $\square$ and $\lozenge$: @@ -70,11 +71,15 @@ They can be seen as counterparts of the derived LTL modalities $\square$ and $\l \erin \begin{definition}[Derived PLTL operators] Given $\phi \in PLTL$, then: - \begin{equation*} - \Fop^{-1} \phi \enspace\defeq\enspace \top \Sop \phi \qquad - \Gop^{-1} \phi \enspace\defeq\enspace \neg \Fop^{-1} \neg \phi + \[ + \begin{array}{rlrl} + \Fop \phi &\defeq \top \Uop \phi \qquad + & \Gop \phi &\defeq \neg \Fop \neg \phi \\ + \Fop^{-1} \phi &\defeq \top \Sop \phi + & \Gop^{-1} \phi &\defeq \neg \Fop^{-1} \neg \phi + \end{array} \qedhere - \end{equation*} + \] \end{definition} Their intuitive meaning is as follows. @@ -145,14 +150,13 @@ we include an arrow that points to the state for which the formula holds. \camil \label{pltl:dual-modalities} -Dual modalities, like the LTL $\square\lozenge$ \enquote{infinitely often} and \enquote{eventually forever}, are less useful in PLTL. +Dual modalities, like the LTL $\square\lozenge$ \enquote{infinitely often} and \enquote{eventually forever}, are less useful with past modalities. $\square^{-1}\lozenge^{-1}\phi$ intuitively holds when at every point in the past, $\phi$ held or there was a previous moment at which $\phi$ held. This is satisfied precisely when $\phi$ held at the first moment in time. Interestingly, $\lozenge^{-1}\square^{-1}\phi$ means the same: it holds when $\phi$ held from the beginning until some moment in the past. -The reason that dual modalities in PLTL are less useful is that we still consider traces with a fixed starting point. +The reason that dual past modalities are less useful is that we still consider traces with a fixed starting point. Thus, while with future modalities it is possible to look infinitely far in the future, it is not possible to look infinitely far in the past. -%TODO: Give examples of semantics along the lines of subsection 5.1.1. Before turning to the formal semantics in the next subsection, we provide some examples of PLTL formulae and their uses. \begin{example}[Properties for a Traffic Light] @@ -164,7 +168,7 @@ Before turning to the formal semantics in the next subsection, we provide some e \[\square\left(\textsl{green} \rightarrow \lnot \Pop\textsl{red}\right) \qedhere\] \end{example} -\begin{example}[Properties for an Authentication System] +\begin{example}[A property for an Authentication System] \label{ex:pltl:authentication-system} \citet{FiterauBrostean2017} use past modalities to describe properties of the Secure Shell (SSH) protocol. One property says that if a channel is opened, there must have been some successful authentication attempt in the past~\citep[p.~149]{FiterauBrostean2017}. @@ -177,4 +181,14 @@ Before turning to the formal semantics in the next subsection, we provide some e The LTL formula is derived algorithmically in \cref{ex:pltl-to-ltl:authentication}. The LTL formula is slightly larger than the PLTL formula and is slightly less understandable. \end{example} + +\begin{remark}[Other Notations] + % TODO: I don't find this place logical for this remark, but it is the same place as Remark 5.16 in the book. + Like for LTL, many different notations are used in literature for PLTL. + These include + $\mathbf X^{-1}, \mathbf G^{-1}, \mathbf F^{-1}$~\citep[e.g.]{Markey2003}, + but also \raisebox{-1pt}{\tikz\draw[black,fill=black](0,0)circle(.4em);}$,\blacksquare,\blacklozenge$~\citep[e.g.]{Gabbay1989} + or $\stackinset{c}{}{c}{}{$\cdot$}{$\bigcirc$},\boxdot,\stackinset{c}{}{c}{}{$\cdot$}{$\lozenge$}$~\citep[e.g.]{Havelund2002}. + % It is always fun to come up with new versions and watch people struggling to reproduce them in \LaTeX. +\end{remark} \cbend |