Organise in different files

12 files changed, 450 insertions, 449 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index 6d79892..027142a 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -83,457 +83,19 @@
 \setcounter{section}{5}
 \setcounter{subsection}{2}
 
-\subsection{Past Modalities in LTL}
-% 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.
-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.
-Only later, when it was shown that past modalities do not increase the expressive power of LTL~\cite{Gabbay1980},
-computing scientists stopped considering past modalities for reasons of minimality.
-
-\erin
-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.}
-	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.
-They are also included in many model checking tools, such as NuSMV.
-For this reason, it is useful to discuss them here.
-\cbend
-
-\subsubsection{Syntax}
-% Provide formal syntax
-% Provide intuitive semantics
-%TODO: Provide formal semantics
-\erin
-This subsection describes the syntax of PLTL.
-PLTL uses the same operators as LTL and adds two additional operators:
-	$\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 $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 \bigcirc \phi
-			\enspace\middle|\enspace \phi_1 \Uop \phi_2
-			\enspace\middle|\enspace \Pop \phi
-			\enspace\middle|\enspace \phi_1 \Sop \phi_2
-			\right.
-	\]
-	where $a \in AP$.
-\end{definition}
-
-\camil
-The precedence order of the operators borrowed from LTL remains the same.
-$\Pop$ binds equally strong as $\Xop$ and $\lnot$.
-$\Sop$ takes precedence over $\Uop$, and like $\Uop$ is right-associative.
-
-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).
-
-\erin
-\begin{definition}[Derived PLTL operators]
-	Given $\phi \in PLTL$, then:
-	\begin{equation*}
-			\Fop^{-1} \phi \defeq \top \Sop \phi \qquad
-			\Gop^{-1} \phi \defeq \neg \Fop^{-1} \neg \phi
-		\qedhere
-	\end{equation*}
-\end{definition}
-
-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 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.
-
-\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{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}\\
-	\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}\\
-	\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}\\
-	\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:PLTL_intuitive}
-\end{figure}
-
-\camil
-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.
-Before turning to the formal semantics in the next subsection, we provide some examples.
-
-\begin{example}[Properties for a Traffic Light]
-	We return to the traffic light of Example 5.4.
-	Since dual past modalities are less useful than dual future modalities, we cannot express the liveness property $\square\lozenge\textsl{green}$ with a pure past formula.
-	However, the requirement \enquote{once red, the light cannot become green immediately} \emph{can} be expressed with past modalities.
-	To rewrite it, consider that this requirements is equivalent to \enquote{if green, the light cannot have been red previously}.
-	This yields the formula:
-	\[\square\left(\textsl{green} \rightarrow \lnot \Pop\textsl{red}\right) \qedhere\]
-\end{example}
-
-\begin{example}[Properties for an 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*}
-\end{example}
-\cbend
-
-\subsubsection{Semantics}
-\erin
-The semantics of LTL and PLTL are defined in a very similar way.
-However, we must make some modifications to the definitions.
-\camil
-In particular, the $\vDash$ operator must be redefined.
-Recall that for LTL we wrote $\sigma \vDash \phi$ when $\sigma$ satisfies $\phi$ and $\sigma[i\dots]$ for the suffix of $\sigma$ starting in the $(j+1)$st symbol.
-The latter notation effectively loses information about the prefix.
-In the case of PLTL, we cannot lose this information.
-For this reason, we use a satisfaction relation at a specific index.
-We will write this as $\sigma \vDash_i \phi$, read as \enquote{$\sigma$ satisfies $\phi$ at $i$}.%
-\footnote{%
-	The notation used in literature varies.
-	\citet{Lichtenstein1985} use $(\sigma,i) \vDash \phi$; \citet{Markey2003} uses $\sigma,i \vDash \phi$.
-	Although the difference is minor, we find $\vDash_i$ more intuitive because it shows that the object being checked is the same in $\sigma\vDash_i\phi$ and $\sigma\vDash_j\phi$.}
-We use $\sigma \vDash \phi$ as a shorthand for $\sigma \vDash_0 \phi$.
-
-\erin
-\begin{definition}[Semantics of PLTL (Interpretation over Words)]
-	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 \vDash \phi\}\]
-	where $\vDash\ \subseteq \left(2^{AP}\right)^\omega \times \mathbb{N} \times PLTL$ is the smallest relation with the properties in \cref{fig:PLTL-semantics}.
-\end{definition}
-\camil
-Note that we must redefine the satisfaction relation for the LTL operators, because $\vDash$ is now a ternary relation.
-The difference with LTL formulae is well illustrated by the $\bigcirc$ operator.
-In the LTL case, $\sigma=A_0A_1A_2\dots\vDash\bigcirc\phi$ iff $\sigma[1\dots]=A_1A_2\dots\vDash\phi$.
-Thus, whether $\bigcirc\phi$ holds for $\sigma$ cannot depend on $A_0$.
-In the PLTL case, $\sigma\vDash_i\bigcirc\phi$ iff $\sigma\vDash_{i+1}\phi$.
-The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\sigma$ may depend on $A_0$,
-	as is trivially the case with $\bigcirc\bigcirc^{-1}a$.
-
-\begin{figure}
-	\centering
-	\begin{mdframed}
-	\[
-		\begin{matrix*}[l]
-			\sigma &\vDash_i & \text{true}\\
-			\sigma &\vDash_i & a                 &\text{iff} & a\in A_i\\
-			\sigma &\vDash_i & \phi_1\land\phi_2 &\text{iff} & \text{$\sigma\vDash_i\phi_1$ and $\sigma\vDash_i\phi_2$}\\
-			\sigma &\vDash_i & \lnot\phi         &\text{iff} & \sigma \nvDash_i \phi\\
-			\sigma &\vDash_i & \bigcirc\phi      &\text{iff} & \sigma \vDash_{i+1} \phi\\
-			\sigma &\vDash_i & \phi_1\Uop\phi_2  &\text{iff} & \exists_{j \le 0}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_i \phi_1$ for all $0 \le i < j$}\\
-			\sigma &\vDash_i & \phi_1\Sop\phi_2  &\text{iff} & \exists_{j \le i}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_k \phi_1$ for all $j < k \le i$}\\
-			\sigma &\vDash_i & \Pop\phi          &\text{iff} & i \geq 1 \wedge \sigma \vDash_{i-1} \phi
-		\end{matrix*}
-	\]
-	\end{mdframed}
-	\caption{PLTL semantics for infinite words $\sigma=A_0A_1A_2\dots \in \left(2^{AP}\right)^\omega$.}
-	\label{fig:PLTL-semantics}
-\end{figure}
-
-\erin
-\begin{definition}[Semantics of PLTL over Paths and States]
-	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 fragments $\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]\]
-			\item $TS$ satisfies $\phi$, denoted by $TS \vDash \phi$ if $Traces \vDash \phi$, if $Traces(TS) \subseteq Words(\phi)$
-				\qedhere
-	\end{itemize}
-\end{definition}
-In order to make these definitions suitable for use with our PLTL operators,
-we must provide their semantics.
-\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.
-
-Given these definitions, it is possible to derive the formal semantics of the $\Fop^{-1}$ and $\Gop^{-1}$ operators as well:
-\[
-	\begin{matrix*}[l]
-		\sigma &\vDash_i &\Fop^{-1}\phi &\text{iff} &\exists_{k \leq i}[\sigma \vDash_k \phi]\\
-		\sigma &\vDash_i &\Gop^{-1}\phi &\text{iff} &\forall_{k \leq i}[\sigma \vDash_k \phi]
-	\end{matrix*}
-\]
-
-\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}
-
-\erin
-\subsubsection{Equivalence of PLTL Formulae}
-Now that we have defined the formal semantics of PLTL,
-we can define equivalence on PLTL formulas.
-
-\begin{definition}[Equivalence of PLTL Formulae]
-	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 \vDash_i \phi \Leftrightarrow \pi \vDash_i \psi \qedhere\]
-\end{definition}
-
-Additionally, we can define another form of equivalence, initial equivalence:
-\begin{definition}[Initial Equivalence of PLTL Formulae]
-	PLTL formulae $\phi_1,\phi_2$ are initially equivalent, denoted $\phi_1 \equiv_0 \phi_2$ iff they verify the following property:
-	\[\text{for any path } \pi, \pi \vDash_0 \phi \Leftrightarrow \pi \vDash_0 \psi \qedhere\]
-\end{definition}
-\cbend
-
-\subsubsection{LTL and PLTL}
-%TODO: Consider/Analyse differences between LTL and PLTL
-
-\subsubsection{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
-
+\input{intro}
+\input{syntax}
+\input{semantics}
+\input{specifying-properties}
+\input{equivalence}
+\input{comparison}
+\input{conversion}
 %TODO: (Section?) Assess if PLTL is actually more succinct using the examples from the SSH Paper
+\input{bad-prefix}
 
-\subsubsection{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?
-
-\subsection{Summary}
-% TODO: points to be added to 5.3
-
-\subsection{Bibliographic Notes}
-% TODO: points to be added to 5.4
-% A possibly helpful list is at https://cstheory.stackexchange.com/a/29452
-% Also the bibliography file should be worked through.
-
-\subsection{Exercises}
-% After the exam documentclass; http://compgroups.net/comp.text.tex/-if-else-fi-in-new-environment/263869
-\newif\ifshowanswers\showanswerstrue
-\newenvironment{answer}%
-	{\ifshowanswers\par\bgroup\small\textit{Answer:}\else\setbox0\vbox\bgroup\fi}%
-	{\egroup}
-\newcommand{\hint}[1]{\par\textit{Hint: #1}}
-\camil
-\begin{exercise}
-	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.
-
-	Take $n\in\mathbb N$ and $AP=\{p_0,\dots,p_n\}$.
-	We first show that there is no polynomial-size LTL formula expressing property~\ref{ex:proof-markey:prop-agreement}.
-	\begin{equation}
-		\phi_n(\sigma) \defeq
-			\forall_{i,j\in\mathbb N}
-			\left[
-				\forall_{k\in[1,n]}
-				[(A_i\vDash p_k) \Leftrightarrow (A_j\vDash p_k)]
-				\rightarrow
-				((A_i\vDash p_0) \Leftrightarrow (A_j\vDash p_0))
-			\right]
-		\label{ex:proof-markey:prop-agreement}
-	\end{equation}
-	where $\sigma=A_0A_1A_2\dots$.
-	In other words, if two points on path $\sigma$ agree on $p_k$ for all $k\in[1,n]$, the points must also agree on $p_0$.
-
-	\begin{enumerate}[label=(\alph*)]
-		\item Find an $\mathcal O\left(2^n\right)$ LTL formula expressing property~\ref{ex:proof-markey:prop-agreement}.
-			\hint{if the formula can be $\mathcal O\left(2^n\right)$, what are you allowed to quantify over?}
-			\begin{answer}%
-				\footnote{Note that this is slightly different from the version in \citet[p. 4]{Markey2003}.
-					The limit on the leftmost $\wedge$ has $i\in[1,n]$ rather than $i\in[0,n]$ in the original paper.
-					We believe this to be an error, because otherwise $a_0$ is a free variable.} %TODO do you agree?
-				\[\phi_n(\sigma) =
-					\bigwedge_{\substack{a_i\in\{\top,\bot\}\\i\in[0,n]}} \left[
-						\left(\lozenge(\bigwedge\nolimits_{i=0}^n p_i=a_i)\right)
-						\rightarrow
-						\square\left((\bigwedge\nolimits_{i=1}^n p_i=a_i) \rightarrow p_0=a_0\right)
-					\right]
-				\]
-			\end{answer}
-
-		\item Assume a polynomial-size LTL formula exists for property~\ref{ex:proof-markey:prop-agreement}.
-			What can you say of the size of a B\"uchi automaton $\mathcal A$ recognizing $\textsl{Words}(\phi_n)$?
-			\label{ex:proof-markey:assumption}
-			\hint{consider Theorem 5.41.}
-			\begin{answer}
-				There exists a B\"uchi automaton of size $\mathcal O(2^{n^k})$ for some $k\in\mathbb N$.
-			\end{answer}
-
-		\item Let $A=a_0,\dots,a_{2^n-1}$ be any permutation of $2^{AP\setminus\{p_0\}}$.
-			Define $w_K=b_{K,0}\dots b_{K,2^n-1}$ with
-			\[
-				b_{K,i} \defeq
-				\begin{cases}
-					a_i              & \text{iff $i\notin K$}\\
-					a_i \cup \{p_0\} & \text{iff $i\in K$.}
-				\end{cases}
-			\]
-			Show that if $K,K' \subseteq \{0,\dots,2^n-1\}$ and $K\ne K'$, also $w_K \ne w_{K'}$.
-			\label{ex:proof-markey:different-w_K}
-			\begin{answer}
-				Without loss of generality, assume there exists an $i\in K$ with $i\notin K'$.
-				Then $p_0\in b_{K,i}$ but $p_0\notin b_{K',i}$.
-				Hence, $w_K\ne w_{K'}$.
-			\end{answer}
-
-		\item How many distinct words $w_K$ exist?
-			\label{ex:proof-markey:nr-of-w_k}
-			\begin{answer}
-				There are $2^{|\{0,\dots,2^n-1\}|} = 2^{2^n}$ distinct $K$ (and equally many distinct $w_K$).
-			\end{answer}
-
-		\item Show that $w_K^\omega$ is accepted by $\mathcal A$.
-			\begin{answer}
-				Since all $a_i$ are distinct,
-					two points $b_{K,j}, b_{K,k}$ on $w_K^\omega$ agree on all $p_i$ for $i\in[1,n]$ iff $j\equiv k \pmod{2^n}$.
-				In this case, they also agree on $p_0$.
-			\end{answer}
-
-		\item It follows that there are paths $\pi_K$ and $\pi_{K'}$ in $\mathcal A$ accepting $w_K^\omega$ and $w_{K'}^\omega$ respectively.
-			Let $q_K$ and $q_{K'}$ be the $2^n$-th states of each of these paths.
-			Assume that $q_K = q_{K'}$.
-			Construct from $w_K$ and $w_{K'}$ an infinite word $v$ that is accepted by $\mathcal A$ but does not satisfy $\phi_n$.
-			\hint{take the simplest infinite word using both words that you can think of.}
-			\begin{answer}
-				Take $v=w_Kw_{K'}^\omega$.
-				Apart from the prefix of size $2^n$, the path of this word is equal to that of $w_{K'}^\omega$, which is accepted.
-				So $v$ is accepted.
-				From \ref{ex:proof-markey:different-w_K} we have an $i$ such that $p_0\in b_{K,i}$ but $p_0\notin b_{K',i}$.
-				However, for all $i\in[1,n]$, $p_i\in b_{K,i} \Leftrightarrow p_i\in b_{K',i}$.
-				Therefore, $i=i, j=i+2^n$ is a counterexample to the outermost quantifier of $\phi_n$.
-			\end{answer}
-
-		\item Show that this contradicts the assumption from \ref{ex:proof-markey:assumption}.
-			\begin{answer}
-				Since we have $2^{2^n}$ distinct $w_K$ [cf. \ref{ex:proof-markey:nr-of-w_k}] and the $2^n$-th states of their accepting paths must all be distinct,
-					$\mathcal A$ has at least $2^{2^n}$ states.
-					But $2^{2^n} \notin \mathcal O(2^{n^k})$.
-			\end{answer}
-
-		\item We now turn to a slightly different property:
-			\begin{equation}
-				\psi_n(\sigma) \defeq
-					\forall_{i\in\mathbb N}
-					\left[
-						\forall_{k\in[1,n]}
-						[(A_i\vDash p_k) \Leftrightarrow (A_0\vDash p_k)]
-						\rightarrow
-						((A_i\vDash p_0) \Leftrightarrow (A_0\vDash p_0))
-					\right]
-				\label{ex:proof-markey:prop-agreement-2}
-			\end{equation}
-			Property \ref{ex:proof-markey:prop-agreement-2} holds if all points on $\sigma$ that agree with all $p_k$ for $k\in[1,n]$ with $A_n$ also agree on $p_0$.
-			Give an $\mathcal O(n)$ PLTL formula expressing property \ref{ex:proof-markey:prop-agreement-2}.
-			\hint{recall the semantics of the dual modalities in PLTL.}
-			\begin{answer}
-				\[\psi_n(\sigma) =
-					\square\left[
-						\left(\bigwedge\nolimits_{i=1}^n (p_i \Leftrightarrow \lozenge^{-1}\square^{-1}p_i)\right)
-						\Rightarrow
-						(p_0 \Leftrightarrow \lozenge^{-1}\square^{-1}p_0)
-					\right]
-				\]
-			\end{answer}
-
-		\item Construct an LTL formula for $\phi_n$ using the PLTL formula for $\psi_n$ and conclude the proof.
-			\hint{first construct an LTL formula for $\psi_n$.}
-			\begin{answer}
-				Take $\phi'_n \defeq \square\psi'_n$, where $\psi'_n$ is an LTL formula initially equivalent to $\psi_n$.
-				By virtue of the $\square$ operator, $\phi_n\equiv\phi'_n$.
-				But $\phi_n$ is $\mathcal O(2^n$, so also $\phi'_n$ is exponential.
-				Since $\phi'_n$ is $\mathcal O(2^n)$ and $\psi_n$ is $\mathcal O(n)$,
-					the PLTL formula for property~\ref{ex:proof-markey:prop-agreement-2} is exponentially more succinct than the LTL formula.
-				\qed
-			\end{answer}
-	\end{enumerate}
-\end{exercise}
-\cbend
+\input{summary}
+\input{bibliographic-notes}
+\input{exercises}
 
 \printbibliography
 
diff --git a/Assignment1/bad-prefix.tex b/Assignment1/bad-prefix.tex
new file mode 100644
index 0000000..98e39ed
--- /dev/null
+++ b/Assignment1/bad-prefix.tex
@@ -0,0 +1,2 @@
+\subsubsection{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?
diff --git a/Assignment1/bibliographic-notes.tex b/Assignment1/bibliographic-notes.tex
new file mode 100644
index 0000000..f4e9cd4
--- /dev/null
+++ b/Assignment1/bibliographic-notes.tex
@@ -0,0 +1,4 @@
+\subsection{Bibliographic Notes}
+% TODO: points to be added to 5.4
+% A possibly helpful list is at https://cstheory.stackexchange.com/a/29452
+% Also the bibliography file should be worked through.
diff --git a/Assignment1/comparison.tex b/Assignment1/comparison.tex
new file mode 100644
index 0000000..5876153
--- /dev/null
+++ b/Assignment1/comparison.tex
@@ -0,0 +1,2 @@
+\subsubsection{LTL and PLTL}
+%TODO: Consider/Analyse differences between LTL and PLTL
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
new file mode 100644
index 0000000..a133fcf
--- /dev/null
+++ b/Assignment1/conversion.tex
@@ -0,0 +1,4 @@
+\subsubsection{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
diff --git a/Assignment1/equivalence.tex b/Assignment1/equivalence.tex
new file mode 100644
index 0000000..6195afc
--- /dev/null
+++ b/Assignment1/equivalence.tex
@@ -0,0 +1,16 @@
+\erin
+\subsubsection{Equivalence of PLTL Formulae}
+Now that we have defined the formal semantics of PLTL,
+we can define equivalence on PLTL formulas.
+
+\begin{definition}[Equivalence of PLTL Formulae]
+	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 \vDash_i \phi \Leftrightarrow \pi \vDash_i \psi \qedhere\]
+\end{definition}
+
+Additionally, we can define another form of equivalence, initial equivalence:
+\begin{definition}[Initial Equivalence of PLTL Formulae]
+	PLTL formulae $\phi_1,\phi_2$ are initially equivalent, denoted $\phi_1 \equiv_0 \phi_2$ iff they verify the following property:
+	\[\text{for any path } \pi, \pi \vDash_0 \phi \Leftrightarrow \pi \vDash_0 \psi \qedhere\]
+\end{definition}
+\cbend
diff --git a/Assignment1/exercises.tex b/Assignment1/exercises.tex
new file mode 100644
index 0000000..cf2a92a
--- /dev/null
+++ b/Assignment1/exercises.tex
@@ -0,0 +1,142 @@
+\subsection{Exercises}
+% After the exam documentclass; http://compgroups.net/comp.text.tex/-if-else-fi-in-new-environment/263869
+\newif\ifshowanswers\showanswerstrue
+\newenvironment{answer}%
+	{\ifshowanswers\par\bgroup\small\textit{Answer:}\else\setbox0\vbox\bgroup\fi}%
+	{\egroup}
+\newcommand{\hint}[1]{\par\textit{Hint: #1}}
+\camil
+\begin{exercise}
+	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.
+
+	Take $n\in\mathbb N$ and $AP=\{p_0,\dots,p_n\}$.
+	We first show that there is no polynomial-size LTL formula expressing property~\ref{ex:proof-markey:prop-agreement}.
+	\begin{equation}
+		\phi_n(\sigma) \defeq
+			\forall_{i,j\in\mathbb N}
+			\left[
+				\forall_{k\in[1,n]}
+				[(A_i\vDash p_k) \Leftrightarrow (A_j\vDash p_k)]
+				\rightarrow
+				((A_i\vDash p_0) \Leftrightarrow (A_j\vDash p_0))
+			\right]
+		\label{ex:proof-markey:prop-agreement}
+	\end{equation}
+	where $\sigma=A_0A_1A_2\dots$.
+	In other words, if two points on path $\sigma$ agree on $p_k$ for all $k\in[1,n]$, the points must also agree on $p_0$.
+
+	\begin{enumerate}[label=(\alph*)]
+		\item Find an $\mathcal O\left(2^n\right)$ LTL formula expressing property~\ref{ex:proof-markey:prop-agreement}.
+			\hint{if the formula can be $\mathcal O\left(2^n\right)$, what are you allowed to quantify over?}
+			\begin{answer}%
+				\footnote{Note that this is slightly different from the version in \citet[p. 4]{Markey2003}.
+					The limit on the leftmost $\wedge$ has $i\in[1,n]$ rather than $i\in[0,n]$ in the original paper.
+					We believe this to be an error, because otherwise $a_0$ is a free variable.} %TODO do you agree?
+				\[\phi_n(\sigma) =
+					\bigwedge_{\substack{a_i\in\{\top,\bot\}\\i\in[0,n]}} \left[
+						\left(\lozenge(\bigwedge\nolimits_{i=0}^n p_i=a_i)\right)
+						\rightarrow
+						\square\left((\bigwedge\nolimits_{i=1}^n p_i=a_i) \rightarrow p_0=a_0\right)
+					\right]
+				\]
+			\end{answer}
+
+		\item Assume a polynomial-size LTL formula exists for property~\ref{ex:proof-markey:prop-agreement}.
+			What can you say of the size of a B\"uchi automaton $\mathcal A$ recognizing $\textsl{Words}(\phi_n)$?
+			\label{ex:proof-markey:assumption}
+			\hint{consider Theorem 5.41.}
+			\begin{answer}
+				There exists a B\"uchi automaton of size $\mathcal O(2^{n^k})$ for some $k\in\mathbb N$.
+			\end{answer}
+
+		\item Let $A=a_0,\dots,a_{2^n-1}$ be any permutation of $2^{AP\setminus\{p_0\}}$.
+			Define $w_K=b_{K,0}\dots b_{K,2^n-1}$ with
+			\[
+				b_{K,i} \defeq
+				\begin{cases}
+					a_i              & \text{iff $i\notin K$}\\
+					a_i \cup \{p_0\} & \text{iff $i\in K$.}
+				\end{cases}
+			\]
+			Show that if $K,K' \subseteq \{0,\dots,2^n-1\}$ and $K\ne K'$, also $w_K \ne w_{K'}$.
+			\label{ex:proof-markey:different-w_K}
+			\begin{answer}
+				Without loss of generality, assume there exists an $i\in K$ with $i\notin K'$.
+				Then $p_0\in b_{K,i}$ but $p_0\notin b_{K',i}$.
+				Hence, $w_K\ne w_{K'}$.
+			\end{answer}
+
+		\item How many distinct words $w_K$ exist?
+			\label{ex:proof-markey:nr-of-w_k}
+			\begin{answer}
+				There are $2^{|\{0,\dots,2^n-1\}|} = 2^{2^n}$ distinct $K$ (and equally many distinct $w_K$).
+			\end{answer}
+
+		\item Show that $w_K^\omega$ is accepted by $\mathcal A$.
+			\begin{answer}
+				Since all $a_i$ are distinct,
+					two points $b_{K,j}, b_{K,k}$ on $w_K^\omega$ agree on all $p_i$ for $i\in[1,n]$ iff $j\equiv k \pmod{2^n}$.
+				In this case, they also agree on $p_0$.
+			\end{answer}
+
+		\item It follows that there are paths $\pi_K$ and $\pi_{K'}$ in $\mathcal A$ accepting $w_K^\omega$ and $w_{K'}^\omega$ respectively.
+			Let $q_K$ and $q_{K'}$ be the $2^n$-th states of each of these paths.
+			Assume that $q_K = q_{K'}$.
+			Construct from $w_K$ and $w_{K'}$ an infinite word $v$ that is accepted by $\mathcal A$ but does not satisfy $\phi_n$.
+			\hint{take the simplest infinite word using both words that you can think of.}
+			\begin{answer}
+				Take $v=w_Kw_{K'}^\omega$.
+				Apart from the prefix of size $2^n$, the path of this word is equal to that of $w_{K'}^\omega$, which is accepted.
+				So $v$ is accepted.
+				From \ref{ex:proof-markey:different-w_K} we have an $i$ such that $p_0\in b_{K,i}$ but $p_0\notin b_{K',i}$.
+				However, for all $i\in[1,n]$, $p_i\in b_{K,i} \Leftrightarrow p_i\in b_{K',i}$.
+				Therefore, $i=i, j=i+2^n$ is a counterexample to the outermost quantifier of $\phi_n$.
+			\end{answer}
+
+		\item Show that this contradicts the assumption from \ref{ex:proof-markey:assumption}.
+			\begin{answer}
+				Since we have $2^{2^n}$ distinct $w_K$ [cf. \ref{ex:proof-markey:nr-of-w_k}] and the $2^n$-th states of their accepting paths must all be distinct,
+					$\mathcal A$ has at least $2^{2^n}$ states.
+					But $2^{2^n} \notin \mathcal O(2^{n^k})$.
+			\end{answer}
+
+		\item We now turn to a slightly different property:
+			\begin{equation}
+				\psi_n(\sigma) \defeq
+					\forall_{i\in\mathbb N}
+					\left[
+						\forall_{k\in[1,n]}
+						[(A_i\vDash p_k) \Leftrightarrow (A_0\vDash p_k)]
+						\rightarrow
+						((A_i\vDash p_0) \Leftrightarrow (A_0\vDash p_0))
+					\right]
+				\label{ex:proof-markey:prop-agreement-2}
+			\end{equation}
+			Property \ref{ex:proof-markey:prop-agreement-2} holds if all points on $\sigma$ that agree with all $p_k$ for $k\in[1,n]$ with $A_n$ also agree on $p_0$.
+			Give an $\mathcal O(n)$ PLTL formula expressing property \ref{ex:proof-markey:prop-agreement-2}.
+			\hint{recall the semantics of the dual modalities in PLTL.}
+			\begin{answer}
+				\[\psi_n(\sigma) =
+					\square\left[
+						\left(\bigwedge\nolimits_{i=1}^n (p_i \Leftrightarrow \lozenge^{-1}\square^{-1}p_i)\right)
+						\Rightarrow
+						(p_0 \Leftrightarrow \lozenge^{-1}\square^{-1}p_0)
+					\right]
+				\]
+			\end{answer}
+
+		\item Construct an LTL formula for $\phi_n$ using the PLTL formula for $\psi_n$ and conclude the proof.
+			\hint{first construct an LTL formula for $\psi_n$.}
+			\begin{answer}
+				Take $\phi'_n \defeq \square\psi'_n$, where $\psi'_n$ is an LTL formula initially equivalent to $\psi_n$.
+				By virtue of the $\square$ operator, $\phi_n\equiv\phi'_n$.
+				But $\phi_n$ is $\mathcal O(2^n$, so also $\phi'_n$ is exponential.
+				Since $\phi'_n$ is $\mathcal O(2^n)$ and $\psi_n$ is $\mathcal O(n)$,
+					the PLTL formula for property~\ref{ex:proof-markey:prop-agreement-2} is exponentially more succinct than the LTL formula.
+				\qed
+			\end{answer}
+	\end{enumerate}
+\end{exercise}
+\cbend
diff --git a/Assignment1/intro.tex b/Assignment1/intro.tex
new file mode 100644
index 0000000..0ccd0ca
--- /dev/null
+++ b/Assignment1/intro.tex
@@ -0,0 +1,25 @@
+\subsection{Past Modalities in LTL}
+% 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.
+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.
+Only later, when it was shown that past modalities do not increase the expressive power of LTL~\cite{Gabbay1980},
+computing scientists stopped considering past modalities for reasons of minimality.
+
+\erin
+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.}
+	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.
+They are also included in many model checking tools, such as NuSMV.
+For this reason, it is useful to discuss them here.
+\cbend
diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex
new file mode 100644
index 0000000..43942b5
--- /dev/null
+++ b/Assignment1/semantics.tex
@@ -0,0 +1,76 @@
+\subsubsection{Semantics}
+\erin
+The semantics of LTL and PLTL are defined in a very similar way.
+However, we must make some modifications to the definitions.
+\camil
+In particular, the $\vDash$ operator must be redefined.
+Recall that for LTL we wrote $\sigma \vDash \phi$ when $\sigma$ satisfies $\phi$ and $\sigma[i\dots]$ for the suffix of $\sigma$ starting in the $(j+1)$st symbol.
+The latter notation effectively loses information about the prefix.
+In the case of PLTL, we cannot lose this information.
+For this reason, we use a satisfaction relation at a specific index.
+We will write this as $\sigma \vDash_i \phi$, read as \enquote{$\sigma$ satisfies $\phi$ at $i$}.%
+\footnote{%
+	The notation used in literature varies.
+	\citet{Lichtenstein1985} use $(\sigma,i) \vDash \phi$; \citet{Markey2003} uses $\sigma,i \vDash \phi$.
+	Although the difference is minor, we find $\vDash_i$ more intuitive because it shows that the object being checked is the same in $\sigma\vDash_i\phi$ and $\sigma\vDash_j\phi$.}
+We use $\sigma \vDash \phi$ as a shorthand for $\sigma \vDash_0 \phi$.
+
+\erin
+\begin{definition}[Semantics of PLTL (Interpretation over Words)]
+	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 \vDash \phi\}\]
+	where $\vDash\ \subseteq \left(2^{AP}\right)^\omega \times \mathbb{N} \times PLTL$ is the smallest relation with the properties in \cref{fig:PLTL-semantics}.
+\end{definition}
+\camil
+Note that we must redefine the satisfaction relation for the LTL operators, because $\vDash$ is now a ternary relation.
+The difference with LTL formulae is well illustrated by the $\bigcirc$ operator.
+In the LTL case, $\sigma=A_0A_1A_2\dots\vDash\bigcirc\phi$ iff $\sigma[1\dots]=A_1A_2\dots\vDash\phi$.
+Thus, whether $\bigcirc\phi$ holds for $\sigma$ cannot depend on $A_0$.
+In the PLTL case, $\sigma\vDash_i\bigcirc\phi$ iff $\sigma\vDash_{i+1}\phi$.
+The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\sigma$ may depend on $A_0$,
+	as is trivially the case with $\bigcirc\bigcirc^{-1}a$.
+
+\begin{figure}
+	\centering
+	\begin{mdframed}
+	\[
+		\begin{matrix*}[l]
+			\sigma &\vDash_i & \text{true}\\
+			\sigma &\vDash_i & a                 &\text{iff} & a\in A_i\\
+			\sigma &\vDash_i & \phi_1\land\phi_2 &\text{iff} & \text{$\sigma\vDash_i\phi_1$ and $\sigma\vDash_i\phi_2$}\\
+			\sigma &\vDash_i & \lnot\phi         &\text{iff} & \sigma \nvDash_i \phi\\
+			\sigma &\vDash_i & \bigcirc\phi      &\text{iff} & \sigma \vDash_{i+1} \phi\\
+			\sigma &\vDash_i & \phi_1\Uop\phi_2  &\text{iff} & \exists_{j \le 0}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_i \phi_1$ for all $0 \le i < j$}\\
+			\sigma &\vDash_i & \phi_1\Sop\phi_2  &\text{iff} & \exists_{j \le i}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_k \phi_1$ for all $j < k \le i$}\\
+			\sigma &\vDash_i & \Pop\phi          &\text{iff} & i \geq 1 \wedge \sigma \vDash_{i-1} \phi
+		\end{matrix*}
+	\]
+	\end{mdframed}
+	\caption{PLTL semantics for infinite words $\sigma=A_0A_1A_2\dots \in \left(2^{AP}\right)^\omega$.}
+	\label{fig:PLTL-semantics}
+\end{figure}
+
+\erin
+\begin{definition}[Semantics of PLTL over Paths and States]
+	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 fragments $\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]\]
+			\item $TS$ satisfies $\phi$, denoted by $TS \vDash \phi$ if $Traces \vDash \phi$, if $Traces(TS) \subseteq Words(\phi)$
+				\qedhere
+	\end{itemize}
+\end{definition}
+In order to make these definitions suitable for use with our PLTL operators,
+we must provide their semantics.
+\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.
+
+Given these definitions, it is possible to derive the formal semantics of the $\Fop^{-1}$ and $\Gop^{-1}$ operators as well:
+\[
+	\begin{matrix*}[l]
+		\sigma &\vDash_i &\Fop^{-1}\phi &\text{iff} &\exists_{k \leq i}[\sigma \vDash_k \phi]\\
+		\sigma &\vDash_i &\Gop^{-1}\phi &\text{iff} &\forall_{k \leq i}[\sigma \vDash_k \phi]
+	\end{matrix*}
+\]
diff --git a/Assignment1/specifying-properties.tex b/Assignment1/specifying-properties.tex
new file mode 100644
index 0000000..0f84a4e
--- /dev/null
+++ b/Assignment1/specifying-properties.tex
@@ -0,0 +1,13 @@
+\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/summary.tex b/Assignment1/summary.tex
new file mode 100644
index 0000000..6f243b2
--- /dev/null
+++ b/Assignment1/summary.tex
@@ -0,0 +1,2 @@
+\subsection{Summary}
+% TODO: points to be added to 5.3
diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex
new file mode 100644
index 0000000..babf688
--- /dev/null
+++ b/Assignment1/syntax.tex
@@ -0,0 +1,153 @@
+\subsubsection{Syntax}
+% Provide formal syntax
+% Provide intuitive semantics
+%TODO: Provide formal semantics
+\erin
+This subsection describes the syntax of PLTL.
+PLTL uses the same operators as LTL and adds two additional operators:
+	$\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 $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 \bigcirc \phi
+			\enspace\middle|\enspace \phi_1 \Uop \phi_2
+			\enspace\middle|\enspace \Pop \phi
+			\enspace\middle|\enspace \phi_1 \Sop \phi_2
+			\right.
+	\]
+	where $a \in AP$.
+\end{definition}
+
+\camil
+The precedence order of the operators borrowed from LTL remains the same.
+$\Pop$ binds equally strong as $\Xop$ and $\lnot$.
+$\Sop$ takes precedence over $\Uop$, and like $\Uop$ is right-associative.
+
+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).
+
+\erin
+\begin{definition}[Derived PLTL operators]
+	Given $\phi \in PLTL$, then:
+	\begin{equation*}
+			\Fop^{-1} \phi \defeq \top \Sop \phi \qquad
+			\Gop^{-1} \phi \defeq \neg \Fop^{-1} \neg \phi
+		\qedhere
+	\end{equation*}
+\end{definition}
+
+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 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.
+
+\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{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}\\
+	\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}\\
+	\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}\\
+	\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:PLTL_intuitive}
+\end{figure}
+
+\camil
+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.
+Before turning to the formal semantics in the next subsection, we provide some examples.
+
+\begin{example}[Properties for a Traffic Light]
+	We return to the traffic light of Example 5.4.
+	Since dual past modalities are less useful than dual future modalities, we cannot express the liveness property $\square\lozenge\textsl{green}$ with a pure past formula.
+	However, the requirement \enquote{once red, the light cannot become green immediately} \emph{can} be expressed with past modalities.
+	To rewrite it, consider that this requirements is equivalent to \enquote{if green, the light cannot have been red previously}.
+	This yields the formula:
+	\[\square\left(\textsl{green} \rightarrow \lnot \Pop\textsl{red}\right) \qedhere\]
+\end{example}
+
+\begin{example}[Properties for an 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*}
+\end{example}
+\cbend