\documentclass[a4paper]{scrartcl}

\title{Model Checking}
\subtitle{Assignment 1}
\author{Camil Staps \and Erin van der Veen}

\begin{document}

\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}