From ebf17c432de4177bf4acd36c2beb6e7bdc5003ef Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Sun, 8 Apr 2018 16:29:24 +0200
Subject: Syntax of LTLP

---
 Assignment1/assignment1.tex | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'Assignment1/assignment1.tex')

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index a7a2eea..78e049c 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -3,6 +3,9 @@
 \usepackage[backend=biber,natbib]{biblatex}
 \bibliography{library}
 
+\usepackage{amsthm}
+\newtheorem{definition}{Definition}
+
 \title{Model Checking}
 \subtitle{Assignment 1}
 \author{Camil Staps \and Erin van der Veen}
@@ -30,9 +33,15 @@ but $\Omega(2^n)$ in LTL.
 Markey achieves this proof by providing an formula that is in exactly this class.
 
 \subsection{Syntax and Semantics}
-%TODO: Provide formal syntax
+% 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:
+\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$$
+\end{definition}
 
 \subsection{LTL and LTL-Past}
 %TODO: Consider/Analyse differences between LTL and LTL-Past
-- 
cgit v1.2.3