Format and TODO

1 files changed, 21 insertions, 0 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index 8463e99..8a274f5 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -9,5 +9,26 @@
 \maketitle
 
 \section{Past Modalities in LTL}
+%TODO: Explain that past Modalities are not necessary for a complete logic
+%TODO: Explain that LTLP does make the logic more succinct (Paper 1)
+%TODO: Give example on what kind of things we want to express with LTLP
+
+\subsection{Syntax and Semantics}
+%TODO: Provide formal syntax
+%TODO: Provide intuitive semantics
+%TODO: Provide formal semantics
+
+\subsection{LTL and LTL-Past}
+%TODO: Consider/Analyse differences between LTL and LTL-Past
+
+\subsection{LTL-Past to LTL}
+%TODO: Provide the syntactic algorithm to convert LTLP to LTL
+%TODO: Provide algorithm via automata to convert LTLP to LTL
+%TODO: In both cases make use of examples from SSH Paper
+
+%TODO: (Section?) Assess if LTLP is actually more succinct using the examples from the SSH Paper
+
+\subsection{Minimal Bad Prefix in NuSMV}
+%TODO: Given a formula of the form vw^\omega, can we find a n \in \mathbb{N} such that vw^n is a bad prefix?
 
 \end{document}