Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking

7 files changed, 134 insertions, 73 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index 1e5a55a..cb1b363 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -78,8 +78,10 @@
 \newif\ifchangebar\changebarfalse
 \let\oldcbend\cbend
 \def\cbend{\oldcbend\changebarfalse}
-\newcommand{\erin}{\ifchangebar\cbend\fi\cbcolor{yellow}\cbstart\changebartrue}
-\newcommand{\camil}{\ifchangebar\cbend\fi\cbcolor{red}\cbstart\changebartrue}
+\newcommand{\changechangebar}[2][2pt]{\ifchangebar\cbend\fi\cbcolor{#2}\cbstart[#1]\changebartrue}
+\newcommand{\erin}{\changechangebar{yellow}}
+\newcommand{\camil}{\changechangebar{red}}
+\newcommand{\both}{\changechangebar[1pt]{orange}}
 
 \renewcommand*{\arraystretch}{1.3}
 
@@ -103,6 +105,7 @@
 
 \begin{document}
 
+\both
 \maketitle
 
 \setcounter{section}{5}
@@ -111,7 +114,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
@@ -121,16 +123,17 @@
 \input{bibliographic-notes}
 \input{exercises}
 
+\both
 \printbibliography
 
 \section*{Contribution}
 %TODO: Like we are some immature group of children, we have to provide proof of contribution
-\camil
 Erin has started writing the text.
 This text was then copy-edited, slightly corrected where needed and expanded by Camil.
 (The result was then copy-edited, slightly corrected where needed and expanded by Erin.
 The result was then copy-edited, slightly corrected where needed and expanded by Camil.)$^\omega$
 In the above, yellow bars indicate content primarily contributed by Erin, whereas red bars indicate content primarily contributed by Camil.
+Thin orange bars indicate material that cannot be attributed to either.
 Unfortunately, disabilities of the \textsf{changebar} package make it impossible to indicate the fine-grainedness of our redaction process.
 \cbend
 
diff --git a/Assignment1/bad-prefix.tex b/Assignment1/bad-prefix.tex
index a2101ba..c9145b3 100644
--- a/Assignment1/bad-prefix.tex
+++ b/Assignment1/bad-prefix.tex
@@ -25,6 +25,7 @@ Once a state reoccurs, $j$ is found.
 This algorithm, more formally described in \cref{alg:bad-prefix}, is obviously guaranteed to find the smallest $i,j$ for which $vw^i$ and $vw^j$ lead to the same state.
 However, it is not guaranteed to find a minimal bad prefix (for instance, when a prefix of $v$ already is a minimal bad prefix).
 
+% TODO: fix placement; see https://tex.stackexchange.com/q/427278/23992
 \begin{algorithm}[H]
 	% NOTE: ugly hardcoded spacing to mimic ugly algorithm layout by Baier-Katoen
 	\caption{Finding a bad prefix for a safety property from a counterexample $vw^\omega$}
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 5fdc04f..1221952 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.
@@ -90,13 +91,13 @@ For the proofs of the equivalences, we refer the reader to the appendix of \cite
 
 \erin
 \begin{enumerate}[resume]
-	\item Suppose $E = q \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
-		% TODO Verify all except 3
+	\item Suppose $E = (q \lor \alpha\Uop\beta) \Sop a$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
 		\begin{align*}
-			E_1 &= (a \wedge \neg \beta \Sop a) \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)\\
-			E_2 &= \neg \beta \wedge \neg \alpha \wedge (\neg \beta \wedge q \Sop a)\\
-			E_3 &= a\Sop\neg\beta \wedge \neg \alpha \wedge q \wedge (q \wedge \neg\beta \Sop a)
+			E_1 &= \bot \Sop a\\
+			E_2 &= (\beta \lor \alpha \land \alpha \Uop \beta) \land (\neg a \lor \neg c) \Sop a\\
+			E_3 &= \neg(\beta \lor \alpha \land \alpha \Uop \beta) \land (\neg a \lor \neg c) \Sop a \land (\neg a \land \neg\beta) \Sop (\neg q \land \neg a)
 		\end{align*}
+		where $c = (\neg a \land \neg\beta) \Sop (\neg q \land \neg a) \land \neg\alpha \land \neg\beta$.
 
 	\item Suppose $E = q \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
 		\begin{align*}
@@ -105,46 +106,58 @@ For the proofs of the equivalences, we refer the reader to the appendix of \cite
 			E_3 &= q \Sop (\neg \alpha \wedge \neg \beta \wedge q \wedge (\neg \beta \wedge q) \Sop a)
 		\end{align*}
 
-	\item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop a$, then $E \equiv \neg (\neg a \Sop \neg q \wedge (\alpha \Uop \beta) \wedge \neg a) \wedge \Fop^{-1} a$,
+	\item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop a$,
+		then $E \equiv \neg (\neg a \Sop (\neg q \wedge (\alpha \Uop \beta) \wedge \neg a)) \wedge \Fop^{-1} a$,
 		which can be reduced via rule 1.
 
-	\item Suppose $E = (q \vee \alpha \Uop \beta) \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \vee (E_2 \wedge E_3)$ where:
+	\item Suppose $E = (q \vee \alpha \Uop \beta) \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \lor E_2 \lor E_3$ where:
 		\begin{align*}
-			E_1 &= (\alpha \Sop a) \wedge (\beta \vee (\alpha \wedge (\alpha \Uop \beta)))\\
-			E_2 &= (\beta \vee \alpha \vee \neg(\neg\beta \Sop \neg q) \Sop \beta \wedge (\alpha \Sop a))\\
-			E_3 &= (\beta \vee (\alpha \wedge (\alpha \Uop \beta))) \vee \neg (\neg\beta \Sop \neg q)
+			E_1 &= \alpha \Sop a \wedge (\beta \vee \alpha \wedge \alpha \Uop \beta)\\
+			E_2 &= \beta \lor \alpha \land \alpha\Uop\beta \land \neg (\neg\alpha \land \neg\beta \land \neg\beta\Sop\neg q) \Sop (\beta \land \alpha \Sop a)\\
+			E_3 &= \neg (\neg\alpha \land \neg\beta \land \neg\beta\Sop\neg q) \Sop (\beta \land \alpha \Sop a) \land (\beta \vee \alpha \wedge \alpha \Uop \beta) \land \neg (\neg\beta \Sop \neg q)
 		\end{align*}
 	
 	\item Suppose $E = (q \vee \alpha \Uop \beta) \Sop (a \wedge \neg(\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
 		\begin{align*}
-			E_1 &= (\neg \beta \wedge q \Sop a) \wedge \neg \beta \wedge \neg \alpha\\
-			E_2 &= q \vee (\alpha \Uop \beta) \Sop \neg \beta \wedge \neg \alpha \wedge (q \vee (\alpha \Uop \beta)) \wedge (\neg \beta \wedge q \Sop a)\\
-			E_3 &= (q \wedge \neg \beta \Sop a) \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)
+			E_1 &= ((\neg \beta \wedge q) \Sop a) \wedge \neg \alpha \wedge \neg \beta\\
+			E_2 &= [q \vee \alpha \Uop \beta] \Sop [\neg \alpha \wedge \neg \beta \wedge (q \vee \alpha \Uop \beta) \wedge (\neg \beta \wedge q) \Sop a]\\
+			E_3 &= (q \wedge \neg \beta) \Sop a \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)
 		\end{align*}
+		$E_2$ has a $\Uop$ in a $\Sop$, but can be further rewritten using elimination 5.
 
 	\item Suppose $E = (q \vee \neg(\alpha \Uop \beta)) \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \vee E_2$ where:
 		\begin{align*}
-			E_1 &= (q \vee \neg (\alpha \Uop \beta) \Sop \beta \wedge (q \vee \neg (\alpha \Uop \beta)) \wedge (\alpha \wedge q \Sop a))\\
-			E_2 &= (\alpha \wedge q \Sop a) \wedge \alpha \wedge (\alpha \Uop \beta)
+			E_1 &= [q \vee \neg (\alpha \Uop \beta)] \Sop [\beta \wedge (q \vee \neg (\alpha \Uop \beta)) \wedge (\alpha \wedge q) \Sop a]\\
+			E_2 &= (\alpha \wedge q) \Sop a \wedge \alpha \wedge \alpha \Uop \beta
 		\end{align*}
 		$E_1$ can be further reduced using eliminations 8 and 4.
-	\item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv \neg \Gop^{-1}(E_1 \vee E_2 \vee E_3)$ where:
+
+	\item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv \neg (E_1 \vee E_2 \vee E_3)$ where:
 		\begin{align*}
-			E_1 &= \neg a \vee \neg (\alpha \Uop \beta)\\
-			E_2 &= \neg a \vee (\alpha \Uop \beta) \Sop \neg q \wedge (\alpha \Uop \beta) \wedge \neg a\\
-			E_3 &= \neg a \vee (\alpha \Uop \beta) \Sop \neg q \wedge (\alpha \Uop \beta)
+			E_1 &= \square^{-1} (\neg a \vee \alpha \Uop \beta)\\
+			E_2 &= (\neg a \vee \alpha \Uop \beta) \Sop (\neg q \wedge \alpha \Uop \beta \wedge \neg a)\\
+			E_3 &= (\neg a \vee \alpha \Uop \beta) \Sop (\neg q \wedge \alpha \Uop \beta)
 		\end{align*}
-		After elimination of $\Gop^{-1}$, this formula can be further eliminated, in particular using elimination 5.
+		\camil
+		Since $\sigma \vDash_i E_2$ entails $\sigma \vDash_i E_3$ for all $i\in\mathbb N$, we also have $E \equiv \neg(E_1 \lor E_3)$.\cbend%
+			\footnote{\cbcolor{red}\cbstart
+				According to \citet[p.~439]{Gabbay1989}, $E_3$ is \enquote{subsumed by} $E_2$.
+				Assuming the straightforward understanding of subsumption ($\phi$ subsumes $\psi$ if and only if $\textsl{Words}(\phi) \supseteq \textsl{Words}(\psi)$), this is incorrect and $E_2$ is subsumed by $E_3$ instead.\cbend}
+		The term\erin\ $E_3$ (and $E_2$) can be further eliminated, in particular using elimination 5.
+		\cbend{}
 \end{enumerate}
+\erin
 
 Note that these rules can only be applied when a $\Uop$ is within the scope of a $\Sop$.
-In order to move the $\Sop$ out of the scope of the $\Uop$, consider that $\Sop$ and $\Uop$ are symmetrical.
-These equivalences also hold when the path is reversed, so similar elimination rules exist for the case that $\Sop$ occurs within the scope of $\Uop$.
+In order to move an $\Sop$ out of the scope of a $\Uop$, consider that $\Sop$ and $\Uop$ are symmetrical.
+The above equivalences also hold when the path is reversed, so similar elimination rules exist for the case that $\Sop$ occurs within the scope of $\Uop$.
 
-The final step of the algorithm entails removing the parts of the formula that contains the $\Sop$-operators.
+The final step of the algorithm entails removing the pure past formulas from the boolean combination.
+After all, these formulas are meaningless for $\vDash_0$, since (using Gabbay's definitions) these formulas can only say things about exclusive past time.
 
 \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)$.
 	This can be rewritten to a form with only $\Uop$ and $\Sop$:
@@ -254,8 +267,31 @@ The final step of the algorithm entails removing the parts of the formula that c
 		\item $\square\lnot(f \land \psi)$.
 			After an authentication failure, a connection cannot be established without prior authentication success.
 	\end{itemize}
-	We see that the formula is reasonably succinct compared to its PLTL version, $\square(c \rightarrow \lnot f \Sop s)$.
-	Using past modalities was not needed in this case.
+	The resulting LTL formula is reasonably succinct, but is clear that the PLTL formula is easier to construct and understand.
+
+	Note that we have not proven that no smaller LTL formula exists.
+	For an example of such a proof, see \cref{ex:succinctness}.
+\end{example}
+
+\begin{example}[Protocol Dependencies]
+	In \cref{ex:pltl:protocol-dependencies}, we considered the PLTL formula
+	$\square \big(\psi \rightarrow
+			\lozenge^{-1} (\phi_3 \land
+				\lozenge^{-1} (\phi_2 \land
+					\lozenge^{-1} \phi_1))\big)$.
+	By the definitions of $\square$ and $\lozenge^{-1}$, it is equivalent to
+	\[
+		\lnot\big(
+			\top \Uop (
+				\psi \land \lnot (
+					\top \Sop (
+						\phi_3 \land \top \Sop (\phi_2 \land \top \Sop \phi_1)
+		)))\big).
+	\]
+	No other temporal operators besides $\Uop$ and $\Sop$ are used, so to transform it to an initially equivalent LTL formula step 1 is not needed.
+
+	Rewriting the formula to Gabbay's definitions and separating the pure past formulas in step 2 proceeds as in the previous example.
+	The exact steps are not shown here for reasons of brevity.
 \end{example}
 
 \erin
@@ -338,6 +374,7 @@ 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.
+<<<<<<< HEAD
 There are multiple ways to convert a NBA to a Muller Automaton.
 In this book we will describe Safra's Determinization Algorithm.
 
diff --git a/Assignment1/exercises.tex b/Assignment1/exercises.tex
index 647755e..ba056d5 100644
--- a/Assignment1/exercises.tex
+++ b/Assignment1/exercises.tex
@@ -64,6 +64,7 @@
 \end{exercise}
 
 \begin{exercise}
+	\label{ex:succinctness}
 	In this exercise we prove that PLTL formulas can be exponentially more succinct.
 	The proof followed here is that of \citet{Markey2003} which, in turn, is based on work by \citet{Etessami2002}.
 	The proof is achieved by giving an example of a formula which can be expressed in $\mathcal O(n)$ in PLTL but requires $\Omega(n)$ in LTL.
diff --git a/Assignment1/intro.tex b/Assignment1/intro.tex
index d07be86..ddbaa5a 100644
--- a/Assignment1/intro.tex
+++ b/Assignment1/intro.tex
@@ -1,8 +1,8 @@
+\erin
 \subsection{Past Modalities in LTL}\label{sec:intro}
 % Explain that past Modalities are not necessary for a complete logic
 % 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
-\erin
 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.
@@ -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 6571564..81a7d7f 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.
@@ -100,8 +105,8 @@ we include an arrow that points to the state for which the formula holds.
 		\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                                (4) [right of=3] {\dots};
+		\node[state,label=$a$,initial below] (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}\\
@@ -110,9 +115,9 @@ we include an arrow that points to the state for which the formula holds.
 		\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[arbitrary]               (3) [right of=2] {};
+		\node[state,label=$a$]         (4) [right of=3] {};
+		\node[arbitrary,initial below] (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}\\
@@ -122,37 +127,39 @@ we include an arrow that points to the state for which the formula holds.
 		\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                          (4) [right of=3] {\dots};
+		\node[arbitrary,initial below] (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}\\
 	\text{was always} & \Gop^{-1} a &
 	\begin{tikzpicture}[intuitive semantics]
-		\node                                (0)              {\dots};
+		\node[state,label=$a$]               (0)              {};
 		\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                                (3) [right of=2] {\dots};
+		\node[state,label=$a$]               (4) [right of=3] {};
+		\node[state,label=$a$,initial below] (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.}
+	\caption{%
+		Intuitive semantics of past modalities.
+		The current state is indicated with an arrow below.
+		All states following the current state are arbitrary.}
 	\label{fig:PLTL_intuitive}
 \end{figure}
 
 \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,19 +171,43 @@ 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}.
 	Also, since that successful authentication, no authentication failure must have occurred.
 	This formula is intuitively expressed by $\square(\textsl{hasOpenedChannel} \rightarrow \lnot \textsl{authFailure} \Sop \textsl{authSuccess})$.
-	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 \textsl{hasOpenedChannel} \Wop\\
-		& \quad (\textsl{authSuccess} \land (\square \textsl{authFailure} \rightarrow \lnot \textsl{hasOpenedChannel} \Uop \textsl{authSuccess}))
-		\qedhere
-	\end{align*}
+	An equivalent LTL formula is $\lnot \psi \land \square\lnot(\textsl{authFailure} \land \psi)$,
+		where $\psi = \lnot\textsl{authSuccess} \Uop (\textsl{hasOpenedChannel} \land \lnot\textsl{authSuccess})$.
+	If $\psi$ holds, a channel will be opened without prior authentication success.
+	Therefore, $\psi$ should not hold at the beginning or when authentication fails.
+	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{example}[Protocol Dependencies]
+	\label{ex:pltl:protocol-dependencies}
+	Past modalities can be useful to describe a protocol in which messages have dependencies.
+	For example, the Secure Shell (SSH) protocol requires that keys have been exchanged between two machines before an authentication request can be handled:
+		if authentication is handled before keys are exchanged, the communication could be intercepted, leaking login details.
+	On an abstract level, there are formulas $\phi_1,\dots,\phi_n,\psi$ and $\psi$ should only hold if $\phi_1,\dots,\phi_n$ held previously (and in that order).
+	In the case of SSH, $\psi$ is the handling of an authentication request;
+		$\phi_1,\dots,\phi_n$ indicate that keys are exchanged correctly.
+	\citet{FiterauBrostean2017} modelled this property using the $\lozenge^{-1}$ modality, which can easily model this dependency.
+	It is here given for $n=3$ (as is the case for SSH):
+	\[
+		\square \big(\psi \rightarrow
+			\lozenge^{-1} (\phi_3 \land
+				\lozenge^{-1} (\phi_2 \land
+					\lozenge^{-1} \phi_1))\big)
+	\]
+\end{example}
+
+\begin{remark}[Other Notations]
+	Like for LTL, many different notations are used in literature for PLTL.
+	These include
+		$\mathbf X^{-1}, \mathbf G^{-1}, \mathbf F^{-1}$~\citep{Markey2003},
+		but also \raisebox{-1pt}{\tikz\draw[black,fill=black](0,0)circle(.4em);}$,\blacksquare,\blacklozenge$~\citep{Gabbay1989}
+		and $\stackinset{c}{}{c}{}{$\cdot$}{$\bigcirc$},\boxdot,\stackinset{c}{}{c}{}{$\cdot$}{$\lozenge$}$~\citep{Havelund2002}.
+\end{remark}
 \cbend