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