LTLP -> PLTL; add SSH example; simplify Tikz; changes to look more like Baier-Katoen; dual modalities

1 files changed, 157 insertions, 114 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index bac6910..8f06b8e 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -11,13 +11,18 @@
 \usepackage{mdframed}
 \usepackage{tikz}
 \usetikzlibrary{automata,positioning}
+\usepackage{relsize}
+\usepackage{cleveref}
+\crefname{figure}{Figure}{Figures}
 
-\newcommand{\defeq}{\overset{\text{def}}{=}}
-\newcommand{\Uop}{\mathbf{U}}
-\newcommand{\Xop}{\mathbf{X}}
-\newcommand{\Sop}{\mathbf{S}}
-\newcommand{\Fop}{\mathbf{F}}
-\newcommand{\Gop}{\mathbf{G}}
+\DeclareMathOperator{\defeq}{\overset{\text{def}}{=}}
+\DeclareMathOperator{\Uop}{\mathbf{U}}
+\DeclareMathOperator{\Wop}{\mathbf{W}}
+\DeclareMathOperator{\Xop}{\bigcirc}
+\DeclareMathOperator{\Fop}{\lozenge}
+\DeclareMathOperator{\Gop}{\square}
+\DeclareMathOperator{\Sop}{\mathbf{S}}
+\DeclareMathOperator{\Pop}{\bigcirc^{--1}}
 
 \title{Model Checking}
 \subtitle{Assignment 1}
@@ -29,141 +34,179 @@
 
 \section{Past Modalities in LTL}
 % Explain that past Modalities are not necessary for a complete logic
-% Explain that LTLP does make the logic more succinct (Paper 1)
-%TODO: Give example on what kind of things we want to express with LTLP
-This section of the book concerns an extension of LTL called ``Past Modalities''.
-The combination of LTL and Past Modalities is often called ``LTL-Past'' or LTLP,
-for the sake of brevity we will use the second (LTLP) to denote this combination.
+% Explain that PLTL does make the logic more succinct (Paper 1)
+%TODO: Give example on what kind of things we want to express with PLTL
+As mentioned in Remark 5.16, LTL can be extended with \emph{past modalities}.
+This section discusses this extension.
+The combination of LTL and Past Modalities is often called \enquote{LTL-Past} or PLTL.
+For the sake of brevity we will use the second (PLTL) to denote this combination.
 When temporal logic was first introduced by Arthur N. Prior in his 1957 book~\cite{Prior1957},
 the logic consisted of both past and future modalities.
 It wasn't until later, after it was shown that past modalities do not increase the expressive power of LTL~\cite{Gabbay1980},
-that computing scientists stopped considering past modalities in favour of minimality.
+that computing scientists stopped considering past modalities for reasons of minimality.
 
-In 2003 Nicolas Markey showed that, while past modalities do not increase expressive power,
-they do make the LTL exponentially more succinct~\cite{Markey2003}.
-In particular, Markey shows that there is a class of LTL-Past formulas that are $O(n)$,
-but $\Omega(2^n)$ in LTL.
-Markey achieves this proof by providing an formula that is in exactly this class.
+However, many properties are most intuitively expressed with past modalities.
+For instance, \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}.
+Also, since that successful authentication, no authentication failure must have occurred.
+This formula is intuitively expressed by $\square(hasOpenedChannel \rightarrow \lnot authFailure \Sop authSuccess)$,
+	assuming $\Sop$ has \enquote{since} semantics.
+Expressing this property in LTL is obscure and tedious.
+One way uses the Weak Until operator from Section 5.1.5:
+%TODO please check that this is actually equivalent
+\begin{align*}
+	& \lnot hasOpenedChannel \Wop\\
+	& \quad (authSuccess \land (\square authFailure \rightarrow \lnot hasOpenedChannel \Uop authSuccess))
+\end{align*}
 
-\subsection{Syntax and Semantics}
+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 formulas 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.
+Thus, the benefit of using past modalities is that it can give a shorter and clearer formula.
+
+\subsection{Syntax}
 % Provide formal syntax
 % Provide intuitive semantics
 %TODO: Provide formal semantics
-This subsection describes the syntax and semantics of LTLP.
-Given that LTLP is an extension of LTL, we are left with two options.
-The first options is to define the entire syntax of LTLP without considering that we have already defined LTL.
-This options is slightly more verbose, but does ensure that this subsection does not depend on the subsection 5.1.1.
-The second option builds on the syntax and semantics that were already defined for LTL formulae.
-It is this option that we will use for this book, since it allows us to focus exclusively on the past modalities that are the focus of this section.
-
-\subsubsection{Syntax}
-\begin{definition}
-	LTLP formulae over the set $LTL$ of LTL formulae are formed according to the following grammar:
-	$$\phi ::= l \mid \phi_1 \Sop \phi_2 \mid \Xop^{-1} \phi$$
+This subsection describes the syntax and semantics of PLTL.%
+\footnote{%
+	Given that PLTL is an extension of LTL, we are left with two options.
+	The first option is to define the entire syntax of PLTL without considering that we have already defined LTL.
+	This option is slightly more verbose, but does not depend on subsection 5.1.1.
+	The second option, which we will adopt here, builds on the syntax and semantics that are already defined for LTL formulae.}
+All LTL formulae are PLTL formulae.
+Two additional operators are added:
+	$\Pop$ (pronounced \enquote{previously}) and
+	$\Sop$ (pronounced \enquote{since}).
+The $\Pop$-modality is comparable to $\Xop$.
+Formula $\Pop\phi$ holds at some moment if $\phi$ held in the previous \enquote{step}.
+The $\Sop$-modality is comparable to $\Uop$: $\phi_1\Sop\phi_2$ holds if $\phi_2$ held at some previous moment
+	and $\phi_1$ held ever after that moment up to and including the current moment.
+
+\begin{definition}[Syntax of PLTL]
+	PLTL formulae over the set $LTL$ of LTL formulae are formed according to the following grammar:
+	$$
+		\phi ::= l
+		\mid \Pop \phi
+		\mid \phi_1 \Sop \phi_2
+	$$
 	where $l \in LTL$.
 \end{definition}
 
-In this grammar, $\Sop$ is the ``since'' operator and $\Xop^{-1}$ is the ``previous'' operator.
-Intuitively, the since operator defines that the second proposition must have occurred continuously since the first occurred.
-The previous operator defines that a proposition must have occurred in the previous state.
+The precedence order of the LTL operators remains the same.
+$\Pop$ binds equally strong as $\Xop$ and $\lnot$.
+$\Sop$ takes precedence over $\Uop$, and like $\Uop$ is right-associative.
 
-Like we did in LTL, we can also derive additional operators in LTLP:
-\begin{definition}
-	Given $\phi \in LTLP$, then\footnote{Note that we assume that the LTL formulas are also extended as given in subsection 5.1.1}:
-	\begin{align*}
-		%\Fop \phi &\defeq \top \Uop \phi\\
-		%\Gop \phi &\defeq \neg \Fop \neg \phi\\
-		\Fop^{-1} \phi &\defeq \top \Sop \phi\\
-		\Gop^{-1} \phi &\defeq \neg \Fop^{-1} \neg \phi
-	\end{align*}
+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$:
+	$\square^{-1}$ (\enquote{was always}, since the beginning until now) and
+	$\lozenge^{-1}$ (\enquote{was sometime}, now or at some point before now).
+
+\begin{definition}[Derived PLTL operators]
+	Given $\phi \in PLTL$, then:
+	$$
+		\Fop^{-1} \phi \defeq \top \Sop \phi \qquad
+		\Gop^{-1} \phi \defeq \neg \Fop^{-1} \neg \phi
+	$$
 \end{definition}
 
-As a result, we can derive the following intuitive meaning for $\Fop^{-1}$ and $\Gop^{-1}$.
+Their intuitive meaning is as follows.
 $\Fop^{-1} \phi$ ensures that at some point in the past $\phi$ was true.
-$\Gop^{-1} \phi$ is satisfied only if it is not true that $\phi$ didn't hold in the past.
-This is equivalent to the fact that $\phi$ held globally until this point.
+$\Gop^{-1} \phi$ is satisfied when there is no moment in the past on which $\phi$ did not hold.
+In other words, $\Gop^{-1}$ entails that $\phi$ held globally until this point.
 
-Figure \ref{fig:LTLP_intuitive} shows the intuitive meanings of the past modalities for the simple case where $a$ and $b$ are the only atomic propositions.
-The left hand side of the figure shows some LTLP formulae,
-the right hand side shows sequences for which this formula trivially holds.
+\Cref{fig:PLTL_intuitive} shows the intuitive meanings of the past modalities for the simple case where $a$ and $b$ are the only atomic propositions.
+The left hand side of the figure shows some PLTL formulae;
+the right hand side shows sequences for which this formula holds.
 Since we need to also consider the past,
 we include an arrow that points to the state for which the formula holds.
 
 \begin{figure}
+	\tikzset{intuitive semantics/.style={shorten >=1pt,node distance=16mm,on grid,initial text={},baseline=-0.5ex,->}}
+	\tikzset{state/.append style={minimum size=15pt}}
+	\tikzset{arbitrary/.style={state,label={[font=\relsize{-2}]arbitrary}}}
 	\centering
-	\begin{align*}
-	a \Sop b&
-	\begin{tikzpicture}[shorten >=1pt,node distance=2cm,on grid,initial text={},baseline=-0.5ex]
-		\node                                          (0)                {\dots};
-		\node[state,label=arbitrary,minimum size=15pt] (1) [right of = 0] {};
-		\node[state,label=$b$      ,minimum size=15pt] (2) [right of = 1] {};
-		\node[state,label=$a$      ,minimum size=15pt] (3) [right of = 2] {};
-		\node[state,label=$a$      ,minimum size=15pt,initial below] (4) [right of = 3] {};
-		\node[state,label=arbitrary,minimum size=15pt] (5) [right of = 4] {};
-		\node                                          (6) [right of = 5] {\dots};
-		\path[->] (0) edge (1) (1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6);
+	\[\begin{array}{rcl}
+	\text{since} & a \Sop b &
+	\begin{tikzpicture}[intuitive semantics]
+		\node                                (0)              {\dots};
+		\node[arbitrary]                     (1) [right of=0] {};
+		\node[state,label=$b$]               (2) [right of=1] {};
+		\node[state,label=$a$]               (3) [right of=2] {};
+		\node[state,label=$a$,initial below] (4) [right of=3] {};
+		\node[arbitrary]                     (5) [right of=4] {};
+		\node                                (6) [right of=5] {\dots};
+		\path (0) edge (1)(1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6);
 	\end{tikzpicture}\\
-	\Xop^{-1} a&
-	\begin{tikzpicture}[shorten >=1pt,node distance=2cm,on grid,initial text={},baseline=-0.5ex]
-		\node                                          (0)                {\dots};
-		\node[state,label=arbitrary,minimum size=15pt] (1) [right of = 0] {};
-		\node[state,label=arbitrary,minimum size=15pt] (2) [right of = 1] {};
-		\node[state,label=$a$      ,minimum size=15pt] (3) [right of = 2] {};
-		\node[state,label=arbitrary,minimum size=15pt,initial below] (4) [right of = 3] {};
-		\node[state,label=arbitrary,minimum size=15pt] (5) [right of = 4] {};
-		\node                                          (6) [right of = 5] {\dots};
-		\path[->] (0) edge (1) (1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6);
+	\text{previously} & \Pop a &
+	\begin{tikzpicture}[intuitive semantics]
+		\node                          (0)              {\dots};
+		\node[arbitrary]               (1) [right of=0] {};
+		\node[arbitrary]               (2) [right of=1] {};
+		\node[state,label=$a$]         (3) [right of=2] {};
+		\node[arbitrary,initial below] (4) [right of=3] {};
+		\node[arbitrary]               (5) [right of=4] {};
+		\node                          (6) [right of=5] {\dots};
+		\path (0) edge (1)(1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6);
 	\end{tikzpicture}\\
-	\Fop^{-1} a&
-	\begin{tikzpicture}[shorten >=1pt,node distance=2cm,on grid,initial text={},baseline=-0.5ex]
-		\node                                          (0)                {\dots};
-		\node[state,label=arbitrary,minimum size=15pt] (1) [right of = 0] {};
-		\node[state,label=$a$      ,minimum size=15pt] (2) [right of = 1] {};
-		\node[state,label=arbitrary,minimum size=15pt] (3) [right of = 2] {};
-		\node[state,label=arbitrary,minimum size=15pt,initial below] (4) [right of = 3] {};
-		\node[state,label=arbitrary,minimum size=15pt] (5) [right of = 4] {};
-		\node                                          (6) [right of = 5] {\dots};
-		\path[->] (0) edge (1) (1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6);
+	\text{was sometime} & \Fop^{-1} a &
+	\begin{tikzpicture}[intuitive semantics]
+		\node                          (0)              {\dots};
+		\node[arbitrary]               (1) [right of=0] {};
+		\node[state,label=$a$]         (2) [right of=1] {};
+		\node[arbitrary]               (3) [right of=2] {};
+		\node[arbitrary,initial below] (4) [right of=3] {};
+		\node[arbitrary]               (5) [right of=4] {};
+		\node                          (6) [right of=5] {\dots};
+		\path (0) edge (1)(1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6);
 	\end{tikzpicture}\\
-	\Gop^{-1} a&
-	\begin{tikzpicture}[shorten >=1pt,node distance=2cm,on grid,initial text={},baseline=-0.5ex]
-		\node                                          (0)                {\dots};
-		\node[state,label=$a$      ,minimum size=15pt] (1) [right of = 0] {};
-		\node[state,label=$a$      ,minimum size=15pt] (2) [right of = 1] {};
-		\node[state,label=$a$      ,minimum size=15pt] (3) [right of = 2] {};
-		\node[state,label=$a$      ,minimum size=15pt,initial below] (4) [right of = 3] {};
-		\node[state,label=arbitrary,minimum size=15pt] (5) [right of = 4] {};
-		\node                                          (6) [right of = 5] {\dots};
-		\path[->] (0) edge (1) (1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6);
-	\end{tikzpicture}\\
-	\end{align*}
+	\text{was always} & \Gop^{-1} a &
+	\begin{tikzpicture}[intuitive semantics]
+		\node                                (0)              {\dots};
+		\node[state,label=$a$]               (1) [right of=0] {};
+		\node[state,label=$a$]               (2) [right of=1] {};
+		\node[state,label=$a$]               (3) [right of=2] {};
+		\node[state,label=$a$,initial below] (4) [right of=3] {};
+		\node[arbitrary]                     (5) [right of=4] {};
+		\node                                (6) [right of=5] {\dots};
+		\path (0) edge (1)(1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6);
+	\end{tikzpicture}
+	\end{array}\]
 	\caption{Intuitive semantics of past modalities.}
-	\label{fig:LTLP_intuitive}
+	\label{fig:PLTL_intuitive}
 \end{figure}
 
+Dual modalities, like the LTL $\square\lozenge$ \enquote{infinitely often} and \enquote{eventually forever}, are less useful in PLTL.
+$\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.
+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.
 
-\subsubsection{Semantics}
-The semantics of LTL and LTLP are defined in a very similar way.
+\subsection{Semantics}
+The semantics of LTL and PLTL are defined in a very similar way.
 We must make some modifications to the Definitions however (in particular to Definition 5.6 and 5.7).
 \begin{definition}
-	Let $\phi$ be a LTLP formula over $AP$. The LT property induced by $\phi$ is
-	$$Words(\phi) = \{\sigma \in (2^{AP})^\omega \mid \sigma,0 \vDash \phi\}$$
-	where $\vDash \subseteq (2^{AP})^\omega \times LTLP$ is the smallest relation with the properties in Figure~\ref{fig:LTLP-semantics} and 5.2.
+	Let $\phi$ be a PLTL formula over $AP$. The LT property induced by $\phi$ is
+	$$Words(\phi) = \{\sigma \in \left(2^{AP}\right)^\omega \mid \sigma,0 \vDash \phi\}$$
+	where $\vDash\ \subseteq \left(2^{AP}\right)^\omega \times PLTL$ is the smallest relation with the properties in \cref{fig:PLTL-semantics} and 5.2.
 \end{definition}
 \begin{definition}
-	Let $TS = (S, Act, \rightarrow, I, AP, L)$ be a transition system without terminal states, and let $\phi$ be an LTLP-formula over AP.
+	Let $TS = (S, Act, \rightarrow, I, AP, L)$ be a transition system without terminal states, and let $\phi$ be an PLTL-formula over AP.
 \begin{itemize}
 	\item For infinite path fragment $\pi$ of $TS$, the satisfaction relation is defined by
 		$$\pi \vDash \phi \Leftrightarrow trace(\pi) \vDash \phi$$
 	\item For state $s \in S$, the satisfaction relation $\vDash$ is defined by
-		$$s \vDash \phi \Leftrightarrow (\forall_{\pi \in Paths(s)}[\pi \vDash \phi]$$
+		$$s \vDash \phi \Leftrightarrow \forall_{\pi \in Paths(s)}[\pi \vDash \phi]$$
 		\item $TS$ satisfies $\phi$, denoted by $TS \vDash \phi$ if $Traces \vDash \phi$, if $Traces(TS) \subseteq Words(\phi)$
 \end{itemize}
 \end{definition}
-In order to make these definitions suitable for use with our LTLP operators,
+In order to make these definitions suitable for use with our PLTL operators,
 we must provide their semantics.
-Figure~\ref{fig:LTLP-semantics} shows the formal semantics of the operators defined in the grammar.
+\Cref{fig:PLTL-semantics} shows the formal semantics of the operators defined in the grammar.
 Note that we need to add a index $i$, since we must also be able to look in the past.
 
 \begin{figure}
@@ -171,13 +214,13 @@ Note that we need to add a index $i$, since we must also be able to look in the
 	\begin{mdframed}
 	$$
 		\begin{matrix*}[l]
-			\sigma,i &\vDash &\phi\Sop\psi &\text{iff} &\exists_{k \leq i}[\sigma,k \vDash \phi \wedge \forall_{k < j \leq i}[\sigma,j \vDash \phi]]\\
-			\sigma,i &\vDash &\Xop^{-1}\phi &\text{iff} &i \geq 1 \wedge \sigma,i-1 \vDash \phi
+			\sigma,i &\vDash &\phi\Sop\psi &\text{iff} &\exists_{k \leq i}[\sigma,k \vDash \psi \wedge \forall_{k < j \leq i}[\sigma,j \vDash \phi]]\\
+			\sigma,i &\vDash &\Pop\phi &\text{iff} &i \geq 1 \wedge \sigma,i-1 \vDash \phi
 		\end{matrix*}
 	$$
 	\end{mdframed}
-	\caption{LTLP semantics for infinite words of $2^{AP}$}
-	\label{fig:LTLP-semantics}
+	\caption{PLTL semantics for infinite words of $2^{AP}$}
+	\label{fig:PLTL-semantics}
 \end{figure}
 
 Given these definitions, it is possible to derive the formal semantics of the $\Fop^{-1}$ and $\Gop^{-1}$ operators as well:
@@ -188,28 +231,28 @@ $$
 	\end{matrix*}
 $$
 
-Now that we have defined the formal semantics of LTLP,
-we can define equivalence on LTLP formulas.
+Now that we have defined the formal semantics of PLTL,
+we can define equivalence on PLTL formulas.
 \begin{definition}
-	LTLP formulae $\phi_1,\phi_2$ are equivalent, denoted $\phi_1 \equiv \phi_2$ iff they verify the following property:
+	PLTL formulae $\phi_1,\phi_2$ are equivalent, denoted $\phi_1 \equiv \phi_2$ iff they verify the following property:
 	$$\text{for any path } \pi \text{ and any position } i, \pi, i \vDash \phi \Leftrightarrow \pi, i \vDash \psi$$.
 \end{definition}
 
 Additionally, we can define another form of equivalence, initial equivalence:
 \begin{definition}
-	LTLP formulae $\phi_1,\phi_2$ are initial equivalent, denoted $\phi_1 \equiv_0 \phi_2$ iff they verify the following property:
+	PLTL formulae $\phi_1,\phi_2$ are initial equivalent, denoted $\phi_1 \equiv_0 \phi_2$ iff they verify the following property:
 	$$\text{for any path } \pi, \pi, 0 \vDash \phi \Leftrightarrow \pi, 0 \vDash \psi$$.
 \end{definition}
 
-\subsection{LTL and LTL-Past}
-%TODO: Consider/Analyse differences between LTL and LTL-Past
+\subsection{LTL and PLTL}
+%TODO: Consider/Analyse differences between LTL and PLTL
 
-\subsection{LTL-Past to LTL}
-%TODO: Provide the syntactic algorithm to convert LTLP to LTL
-%TODO: Provide algorithm via automata to convert LTLP to LTL
+\subsection{PLTL to LTL}
+%TODO: 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
 
-%TODO: (Section?) Assess if LTLP is actually more succinct using the examples from the SSH Paper
+%TODO: (Section?) Assess if PLTL is actually more succinct using the examples from the SSH Paper
 
 \subsection{Minimal Bad Prefix in NuSMV}
 %TODO: Given a formula of the form vw^\omega, can we find a n \in \mathbb{N} such that vw^n is a bad prefix?