Extend syntax

1 files changed, 14 insertions, 10 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index e58ed6b..c00caf6 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -44,22 +44,26 @@ Markey achieves this proof by providing an formula that is in exactly this class
 % Provide formal syntax
 %TODO: Provide intuitive semantics
 %TODO: Provide formal semantics
-Let $P$ be the set of atomic propositions $\{p, q, r, \dots\}$, 
-then the syntax of LTLP is defined as:
+This subsection describes the syntax and semantics of LTLP.
+Given that LTLP is an extension of LTL, we are left with two options.
+The first options is to define the entire syntax of LTLP without considering that we have already defined LTL.
+This options is slightly more verbose, but does ensure that this subsection does not depend on the subsection 5.1.1.
+The second option builds on the syntax and semantics that were already defined for LTL formulae.
+It is this option that we will use for this book, since it allows us to focus exclusively on the past modalities that are the focus of this section.
+
 \begin{definition}
-	Given $\phi, \psi \in LTLP$, then:
-	$$LTLP ::= \neg\phi \mid \phi \vee \psi \mid \phi \Uop \psi \mid \Xop \phi \mid \phi \Sop \psi \mid \Xop^{-1} \phi \mid p \mid q$$
+	LTLP formulae over the set $LTL$ of LTL formulae are formed according to the following grammar:
+	$$\phi ::= l \mid \phi_1 \Sop \phi_2 \mid \Xop^{-1} \phi$$
+	where $l \in LTL$.
 \end{definition}
 Additionally, we extend LTLP further with the following abbreviations:
 \begin{definition}
-	Given $\phi \in LTLP$, then:
+	Given $\phi \in LTLP$, then\footnote{Note that we assume that the LTL formulas are also extended as given in subsection 5.1.1}:
 	\begin{align*}
-		\Fop \phi &\defeq \top \Uop \phi\\
-		\Gop \phi &\defeq \neg \Fop \neg \phi\\
+		%\Fop \phi &\defeq \top \Uop \phi\\
+		%\Gop \phi &\defeq \neg \Fop \neg \phi\\
 		\Fop^{-1} \phi &\defeq \top \Sop \phi\\
-		\Gop^{-1} \phi &\defeq \neg \Fop^{-1} \neg \phi
-	\end{align*}
-	Where $\top$ is the atomic proposition that is always true.
+		\Gop^{-1} \phi &\defeq \neg \Fop^{-1} \neg \phi	\end{align*}
 \end{definition}
 
 \subsection{LTL and LTL-Past}