1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
\documentclass[a4paper]{scrartcl}
\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}
\begin{document}
\maketitle
\section{Past Modalities in LTL}
% Explain that past Modalities are not necessary for a complete logic
% 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
This section of the book concerns an extension of LTL called ``Past Modalities''.
The combination of LTL and Past Modalities is often called ``LTL-Past'' or LTLP,
for the sake of brevity (and without compromising readability) we will use the first (LTL-Past) to denote this combination.
When temporal logic was first introduced by Arthur N. Prior in his 1957 book~\cite{Prior1957},
the logic consisted of both past and future modalities.
It wasn't until later, after it was shown that past modalities do not increase the expressive power of LTL~\cite{Gabbay1980},
that computing scientists stopped considering past modalities in favour of minimality.
In 2003 Nicolas Markey showed that, while past modalities do not increase expressive power,
they do make the LTL exponentially more succinct~\cite{Markey2003}.
In particular, Markey shows that there is a class of LTL-Past formulas that are $O(n)$,
but $\Omega(2^n)$ in LTL.
Markey achieves this proof by providing an formula that is in exactly this class.
\subsection{Syntax and Semantics}
% 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
\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?
\section{Contribution}
%TODO: Like we are some immature group of children, we have to provide proof of contribution
\printbibliography
\end{document}
|
