Add contribution annotations

1 files changed, 31 insertions, 2 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index f10d767..d5de1a7 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -44,6 +44,13 @@
 \usepackage{parskip}
 \usepackage{cleveref}
 \crefname{figure}{Figure}{Figures}
+\usepackage[color]{changebar}
+\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}
+
 \renewcommand*{\arraystretch}{1.3}
 
 \DeclareMathOperator{\defeq}{\overset{\text{def}}{=}}
@@ -67,15 +74,17 @@
 % 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.
-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.
+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%
@@ -85,11 +94,13 @@ 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
 
 \subsection{Syntax}
 % Provide formal syntax
 % Provide intuitive semantics
 %TODO: Provide formal semantics
+\erin
 This subsection describes the syntax and semantics of PLTL.%
 \footnote{%
 	Given that PLTL is an extension of LTL, we are left with two options.
@@ -115,6 +126,7 @@ The $\Sop$-modality is comparable to $\Uop$: $\phi_1\Sop\phi_2$ holds if $\phi_2
 	where $l \in LTL$.
 \end{definition}
 
+\camil
 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.
@@ -124,6 +136,7 @@ They can be seen as counterparts of the derived LTL modalities $\square$ and $\l
 	$\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*}
@@ -199,6 +212,7 @@ we include an arrow that points to the state for which the formula holds.
 	\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.
@@ -232,10 +246,13 @@ Before turning to the formal semantics in the next subsection, we provide some e
 		\qedhere
 	\end{align*}
 \end{example}
+\cbend
 
 \subsection{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.
@@ -248,11 +265,13 @@ We will write this as $\sigma \vDash_i \phi$, read as \enquote{$\sigma$ satisfie
 	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.
 
 \begin{figure}
@@ -275,6 +294,7 @@ Note that we must redefine the satisfaction relation for the LTL operators, beca
 	\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}
@@ -311,6 +331,7 @@ Additionally, we can define another form of equivalence, initial equivalence:
 	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 \vDash_0 \phi \Leftrightarrow \pi \vDash_0 \psi \qedhere\]
 \end{definition}
+\cbend
 
 \subsection{LTL and PLTL}
 %TODO: Consider/Analyse differences between LTL and PLTL
@@ -334,6 +355,14 @@ Additionally, we can define another form of equivalence, initial equivalence:
 
 \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.
+Unfortunately, disabilities of the \textsf{changebar} package make it impossible to indicate the fine-grainedness of our redaction process.
+\cbend
 
 \printbibliography