Styling

1 files changed, 70 insertions, 34 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index 8f06b8e..65b5bad 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -6,7 +6,34 @@
 \usepackage{amsmath}
 \usepackage{amsthm}
 \usepackage{amssymb}
-\newtheorem{definition}{Definition}
+% See http://www.ams.org/faq?faq_id=212 for the trick to add qed at the end of
+% definitions and examples.
+\newtheoremstyle{mydefinition}%
+	{1em}{1em}% Style above and below
+	{}% Body font
+	{}% Indent
+	{\bfseries}% Theorem head font
+	{}% Punctuation after theorem head
+	{0pt}% Space after theorem head
+	{\thmname{#1}\thmnumber{ #2}.\quad #3\\[4pt]}% Theorem head spec
+\theoremstyle{mydefinition}
+\newtheorem{xdefinition}{Definition}
+\newtheoremstyle{myexample}%
+	{1em}{1em}% Style above and below
+	{}% Body font
+	{}% Indent
+	{\itshape}% Theorem head font
+	{}% Punctuation after theorem head
+	{0pt}% Space after theorem head
+	{\thmname{#1}\thmnumber{ #2}.\quad #3\\[4pt]}% Theorem head spec
+\theoremstyle{myexample}
+\newtheorem{xexample}{Example}
+\newenvironment{definition}%
+	{\renewcommand{\qedsymbol}{$\blacksquare$}\pushQED{\qed}\begin{xdefinition}}%
+	{\popQED\end{xdefinition}}
+\newenvironment{example}%
+	{\renewcommand{\qedsymbol}{$\blacksquare$}\pushQED{\qed}\begin{xexample}}%
+	{\popQED\end{xexample}}
 \usepackage{mathtools}
 \usepackage{mdframed}
 \usepackage{tikz}
@@ -45,25 +72,15 @@ 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 for reasons of minimality.
 
-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*}
-
 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)$.
+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.
-Thus, the benefit of using past modalities is that it can give a shorter and clearer formula.
+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.
 
 \subsection{Syntax}
 % Provide formal syntax
@@ -105,10 +122,11 @@ They can be seen as counterparts of the derived LTL modalities $\square$ and $\l
 
 \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
-	$$
+	\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.
@@ -185,24 +203,42 @@ The reason that dual modalities in PLTL are less useful is that we still conside
 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 an authentication system]
+	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))
+		\qedhere
+	\end{align*}
+\end{example}
 
 \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}
+\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,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}
+\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 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]$$
-		\item $TS$ satisfies $\phi$, denoted by $TS \vDash \phi$ if $Traces \vDash \phi$, if $Traces(TS) \subseteq Words(\phi)$
-\end{itemize}
+	\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]$$
+			\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.
@@ -233,15 +269,15 @@ $$
 
 Now that we have defined the formal semantics of PLTL,
 we can define equivalence on PLTL formulas.
-\begin{definition}
+\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, i \vDash \phi \Leftrightarrow \pi, i \vDash \psi$$.
+	\[\text{for any path } \pi \text{ and any position } i, \pi, i \vDash \phi \Leftrightarrow \pi, i \vDash \psi \qedhere\]
 \end{definition}
 
 Additionally, we can define another form of equivalence, initial equivalence:
-\begin{definition}
+\begin{definition}[Initial Equivalence of PLTL Formulae]
 	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$$.
+	\[\text{for any path } \pi, \pi, 0 \vDash \phi \Leftrightarrow \pi, 0 \vDash \psi \qedhere\]
 \end{definition}
 
 \subsection{LTL and PLTL}