Extend LTLP syntax

1 files changed, 20 insertions, 1 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index 78e049c..e58ed6b 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -3,9 +3,17 @@
 \usepackage[backend=biber,natbib]{biblatex}
 \bibliography{library}
 
+\usepackage{amsmath}
 \usepackage{amsthm}
 \newtheorem{definition}{Definition}
 
+\newcommand{\defeq}{\overset{\text{def}}{=}}
+\newcommand{\Uop}{\mathbf{U}}
+\newcommand{\Xop}{\mathbf{X}}
+\newcommand{\Sop}{\mathbf{S}}
+\newcommand{\Fop}{\mathbf{F}}
+\newcommand{\Gop}{\mathbf{G}}
+
 \title{Model Checking}
 \subtitle{Assignment 1}
 \author{Camil Staps \and Erin van der Veen}
@@ -40,7 +48,18 @@ Let $P$ be the set of atomic propositions $\{p, q, r, \dots\}$,
 then the syntax of LTLP is defined as:
 \begin{definition}
 	Given $\phi, \psi \in LTLP$, then:
-$$LTLP ::= \neg\phi \mid \phi \vee \psi \mid \phi \mathbf{U} \psi \mid \mathbf{X} \phi \mid \phi \mathbf{S} \psi \mid \mathbf{X}^{-1} \phi \mid p \mid q$$
+	$$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$$
+\end{definition}
+Additionally, we extend LTLP further with the following abbreviations:
+\begin{definition}
+	Given $\phi \in LTLP$, then:
+	\begin{align*}
+		\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.
 \end{definition}
 
 \subsection{LTL and LTL-Past}