Start with editing of the syntactic algorithm for PLTL -> LTL

1 files changed, 117 insertions, 53 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 544e0b4..1786b5d 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -1,105 +1,169 @@
 \erin
 \subsubsection{PLTL to LTL}
-In Subsection~\ref{sec:intro} we stated that past modalities do not increase the expressive power of LTL.
-In this section we proof this statement by demonstrating two algorithms that can convert any arbitrary PLTL formula to a LTL formula.
-The first algorithm that we will demonstrate was first presented by Gabbay in 1989~\cite{Gabbay1989} and is based on syntactic rewriting.
+Above, we stated that past modalities do not increase the expressive power of LTL.
+In this section we prove this statement by demonstrating two algorithms that can convert a arbitrary PLTL formulas to initially equivalent LTL formulas.
+The first algorithm was first presented by \citet{Gabbay1989} in 1989 and is based on syntactic rewriting.
 The second algorithm makes use of the translation of PLTL formulas to automata and automata to LTL formulas.
-We will explain more about this algorithm once we get to it.
+This algorithm is described in more detail below.
 
-\erin
 \paragraph{Syntactic Algorithm}
-The syntactic algorithm as proposed by Gabby has its foundation in the following three facts\footnote{Note that Gabbay used a slightly different definition for the $\Uop$ and $\Sop$ operators. For this paragraph of the book we will assume $\phi \Uop \psi := \Xop (\phi \Uop \psi)$ and $\phi \Sop \psi := \Xop^{-1} (\phi \Sop \psi)$. For a given formula, it is not hard to convert it to this form.}:
+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.
+		\camil
+		We then get $\sigma \vDash_i \phi_1 \Uop \phi_2 \Leftrightarrow \exists_{j > i}[\sigma \vDash_j \phi_2]$ and $\sigma \vDash_k \phi_1$ for all $i < k < j$ (rather than $i \le k < j$), and similarly for $\Sop$.
+		Thus, our $\phi \Uop \psi$ is equivalent to Gabbay's $\psi \lor \phi \land \phi \Uop \psi$.
+		Gabbay's $\phi \Uop \psi$ is equivalent to our $\Xop (\phi \Uop \psi)$.
+		Also for the $\Sop$ operator is not hard to convert PLTL formulas with the semantics of \cref{def:pltl:semantics-words} to Gabbay's variant or vice versa.
+		\erin
+		For this paragraph we will use Gabbay's definitions.}
 \begin{enumerate}
-	\item Every PLTL formula can be written using only the $\Sop$ and $\Uop$ operators.
-	\item Every formula containing only the $\Sop$ and $\Uop$ operators can be written in the following form: $F \cup P \cup A$ where $F$ are the future modalities ($\Uop$), $P$ are the past modalities ($\Sop$), and $A$ are the atomic expressions.
-	\item When removing $P$ from this formula, the resulting formula is equivalent to the formula we started with when applied on position 0 in the path.
+	\item Every PLTL formula can be written using no other temporal operators than $\Sop$ and $\Uop$ operators.
+	\item Every formula $\phi$ containing only the $\Sop$ and $\Uop$ operators can be written as a boolean combination of $\wfff \cup \wffp \cup \wffn$.
+	\item The same formula without past modalities $\psi$, a boolean combination of $\wfff \cup \wffn$, is initially equivalent to $\phi$.
 \end{enumerate}
 When these facts are considered in sequence,
-it is trivial to realise that it results in an algorithm that, given a PLTL formula, produces an initially equivalent LTL formula.
-We will now show these facts in more detail.
-
-Step 1 of the algorithm is trivially given using a rewrite system.
-This rewrite system is given in Figure~\ref{fig:rewrite}.
-\begin{figure}
-	\centering
-	\begin{alignat*}{2}
-		&\Pop\phi       &&\leftrightarrow \bot \Sop \phi\\
-		&\Xop\phi       &&\leftrightarrow \bot \Uop \phi\\
-		&\Gop\phi       &&\leftrightarrow \neg (\top \Uop \neg \phi)\\
-		&\Fop\phi       &&\leftrightarrow \top \Uop \phi\\
-		&\Gop^{-1}\phi &&\leftrightarrow \neg (\top \Sop \neg \phi)\\
-		&\Fop^{-1}\phi &&\leftrightarrow \top \Sop \neg
-	\end{alignat*}
-	\caption{The rewrite rules for writing any PLTL formula as a formula containing only $\Sop$ and $\Uop$.}
-	\label{fig:rewrite}
-\end{figure}
-This full expressiveness of $\Uop$ and $\Sop$ is proven in the PhD. thesis of J. Kamp~\cite{Kamp1968},
-and again by Gabbay using a different method~\cite{Gabbay1989}.
-
-Step 2 of the algorithm entails rewriting the formula containing only $\Uop$ and $\Sop$ to a form where there is no $\Sop$ in the scope of a $\Uop$,
-and there exists on $\Uop$ in the scope of a $\Sop$.
-Gabby proofs that this can by done in Theorem 2.4 of his paper,
-the rewrite rules are given in the Appendix of the same paper.
-In this book, we will not proof that these rewrite rules hold, but they are given below.
+they result in an algorithm that, given a PLTL formula, produces an initially equivalent LTL formula.
+We will now consider these facts in more detail.
+
+Step 1 of the algorithm was proven by Kamp in is 1968 PhD thesis \citep{Kamp1968}.
+It can also be shown by a set of rewrite rules, the approach taken by \citet{Gabbay1989}.
+The correctness then follows from the formal semantics of the operators.
+We only need to rewrite $\Xop$ and $\Xop^{-1}$.
+Gabbay also gives rewrite rules for $\square$, $\lozenge$ and their PLTL counterparts, but since we have defined them as derived operators this is not necessary.
+The next and previous operators can be rewritten as:
+\[
+	\begin{array}{ll}
+		\Pop\phi &\rightarrow\enspace \bot \Sop \phi\\
+		\Xop\phi &\rightarrow\enspace \bot \Uop \phi
+	\end{array}
+\]
+
+Step 2 of the algorithm entails rewriting the formula containing only $\Uop$ and $\Sop$ to a form where there is no $\Sop$ in the scope of a $\Uop$, nor vice versa.
+Gabbay proves that this can by done in Theorem 2.4 of his paper via a tedious case distinction.
+The different cases are listed below.
+For the proofs of the equivalences, we refer the reader to the appendix of \citet{Gabbay1989}.
 \begin{enumerate}
-	\item Suppose $E = q \Sop a \wedge (\alpha \Uop \beta))$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
+	\item Suppose $E = q \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
 		\begin{align*}
-			E_1 &= (q \Sop a) \wedge (\alpha \Sop a) \wedge \alpha (\alpha \Uop \beta)\\
-			E_2 &= \beta \wedge (\alpha \Sop a) \wedge (q \Sop a)\\
-			E_3 &= q \Sop \beta \wedge q \wedge (\alpha \Sop a) \wedge (q \Sop a)
+			E_1 &= q \Sop a \wedge \alpha \Sop a \wedge \alpha \wedge \alpha \Uop \beta\\
+			E_2 &= \beta \wedge (\alpha \wedge q) \Sop a\\
+			E_3 &= q \Sop (\beta \wedge q \wedge \alpha \Sop a \wedge q \Sop a)
 		\end{align*}
+\end{enumerate}
 
-	\item Suppose $E = q \Sop a \wedge \neg (\alpha \Uop \beta)$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
+\camil
+\begin{remark}[Intuition Behind the Elimination Rules]
+	The intuition behind Gabbay's first elimination rule is as follows.
+	If $q \Sop (a \land \alpha \Uop \beta)$, we know that at some point $t$, $a$ held, and that after $t$, $q$ held until the present moment.
+	For the moment of fulfilment of $\alpha \Uop \beta$ we distinguish three cases:
+	\begin{enumerate}
+		\item
+			$\alpha$ continuously held since $t$, presently holds, and continues to hold until at some point in the future $\beta$ holds.
+		\item
+			$\alpha$ has held since $t$ and at present $\beta$ holds.
+		\item
+			$\alpha$ has held since $t$ until some moment in the past at which $\beta$ held.
+	\end{enumerate}
+	These cases correspond to the elements of the disjunction $E_1$, $E_2$ and $E_3$, respectively.
+	Note that case 2 and 3 are only different because of Gabbay's non-strict semantics.
+
+	It is now easy to reconstruct the case where $\Sop$ and $\Uop$ are swapped, i.e. $E = q \Uop (a \land \alpha \Sop \beta)$.
+	In this case, $q$ holds from the next moment until some moment $t$ at which $a$ will hold.
+	For the moment of fulfilment of $\alpha \Sop \beta$ we distinguish three cases:
+	\begin{enumerate}
+		\item
+			$\beta$ held at some moment in the future. $\alpha$ held continuously after that moment, including the present moment and up to $t$.
+		\item
+			$\beta$ currently holds and $\alpha$ continuously holds until $t$.
+		\item
+			At some point in the future (before $t$), $\beta$ will hold, after which $\alpha$ continuously holds until $t$.
+	\end{enumerate}
+	Thus we get $E \equiv E_1 \lor E_2 \lor E_3$ where:
+	\begin{align*}
+		E_1 &= q \Uop a \land \alpha \Uop a \land \alpha \land \alpha \Sop \beta\\
+		E_2 &= \beta \land (q \land \alpha) \Uop a\\
+		E_3 &= q \Uop (\beta \land q \land \alpha \Uop a \land q \Uop a)
+	\end{align*}
+	The reasoning behind the other elimination rules is similar and will not be discussed in detail.
+\end{remark}
+
+\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:
 		\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)
 		\end{align*}
 
-	\item Suppose $E = q \Sop a \wedge \neg (\alpha \Sop \beta)$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
+	\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*}
 			E_1 &= (q \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 &= q \Sop (\neg \beta \wedge \neg \alpha \wedge q \wedge (\neg \beta \wedge q \Sop a))
 		\end{align*}
 
-	\item Suppose $E = q \vee \neg (\alpha \Uop \beta) \Sop a$ then it holds that $E = \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 it holds that $E = E_1 \vee (E_2 \wedge E_3)$ if:
+	\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:
 		\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)
 		\end{align*}
 	
-	\item Suppose $E = q \vee (\alpha \Uop \beta) \Sop a \wedge \neg(\alpha \Uop \beta)$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
+	\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)
 		\end{align*}
 
-	\item Suppose $E = q \vee \neg(\alpha \Uop \beta) \Sop a \wedge (\alpha \Uop \beta)$ then it holds that $E = E_1 \vee E_2$ if:
+	\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)
 		\end{align*}
-		Where $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 it holds that $E = \neg \Gop^{-1}(E_1 \vee E_2 \vee E_3)$ if:
+		$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:
 		\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)
 		\end{align*}
-		After elimination of $\Gop^{-1}$, this formula can be further eliminated.
-		In particular by using elimination 5.
+		After elimination of $\Gop^{-1}$, this formula can be further eliminated, in particular using elimination 5.
 \end{enumerate}
-When considering these rules, it might be noted that they 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$ we need to consider that these formulas also hold when the path is reversed.
-I.e. we can also apply these eliminations when a $\Sop$ is within the scope of a $\Uop$.
 
-The final step of the algorithm entails removing the part of the formula that contains the $\Sop$-operators.
+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$.
+
+The final step of the algorithm entails removing the parts of the formula that contains the $\Sop$-operators.
+
+\camil
+\begin{example}[Properties for an Authentication System]
+	Consider again the property from \cref{ex:pltl:authentication-system}, repeated here with less verbose names:
+	$\square (c \rightarrow \lnot f \Sop s)$.
+	This can be rewritten to a form with only $\Uop$ and $\Sop$:
+	\begin{align*}
+		\square(c \rightarrow \lnot f \Sop s)
+		&\equiv \lnot \lozenge \lnot (c \rightarrow \lnot f \Sop s)\\
+		&\equiv \lnot (\top \Uop (\lnot (c \rightarrow \lnot f \Sop s)))\\
+		&\equiv \lnot (\top \Uop (c \land \lnot (\lnot f \Sop s))).
+	\end{align*}
+	With Gabbay's $\Uop$ and $\Sop$, this becomes (first rewriting the $\Sop$, then the $\Uop$):
+	\begin{align*}
+		\lnot (\top \Uop (c \land \lnot(\lnot f \Sop s)))
+		&\rightarrow \lnot (\top \Uop (c \land \lnot(s \lor \lnot f \land \lnot f \Sop s)))\\
+		&\equiv \lnot (\top \Uop (c \land \lnot s \land f \land \lnot (\lnot f \Sop s))) \\
+		&\rightarrow \lnot ((c \land \lnot s \land f \land \lnot (\lnot f \Sop s)) \lor (\top \Uop (c \land \lnot s \land f \land \lnot (\lnot f \Sop s))))\\
+		&\equiv \lnot (c \land \lnot s \land f \land \lnot (\lnot f \Sop s)) \land \lnot(\top \Uop (c \land \lnot s \land f \land \lnot (\lnot f \Sop s)))\\
+		&\equiv (\lnot c \lor s \lor \lnot f \Sop s) \land \lnot(\top \Uop (c \land \lnot s \land f \land \lnot (\lnot f \Sop s))).
+	\end{align*}
+	% TODO: step 2 and 3 on the right part (S nested in U)
+\end{example}
 
 \erin
 \paragraph{Automata-based Algorithm}