blob: 449615de9e484c5209c3a7867068b89f94435666 (
plain) (
blame)
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
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
\documentclass[a4paper,parskip=half]{scrartcl}
\usepackage[backend=biber,natbib]{biblatex}
\bibliography{library}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}
\renewcommand{\qedsymbol}{$\blacksquare$}
\let\leq\leqslant
\let\le\leqslant
\let\geq\geqslant
\let\ge\geqslant
% See http://www.ams.org/faq?faq_id=212 for the trick to add qed at the end of
% definitions and examples.
\newtheoremstyle{mydefinition}%
{2em}{2em}% Space above and below
{}% Body font
{}% Indent
{\bfseries}% Theorem head font
{}% Punctuation after theorem head
{0pt}% Space after theorem head
{\thmname{#1}\thmnumber{ #2}.\quad #3\\[4pt]}% Theorem head spec
\theoremstyle{mydefinition}
\newtheorem{xdefinition}{Definition}
\newenvironment{definition}%
{\pushQED{\qed}\begin{xdefinition}}%
{\popQED\end{xdefinition}}
\newtheoremstyle{myexample}%
{2em}{2em}% Space above and below
{}% Body font
{}% Indent
{\itshape}% Theorem head font
{}% Punctuation after theorem head
{0pt}% Space after theorem head
{\thmname{#1}\thmnumber{ #2}.\quad #3\\[4pt]}% Theorem head spec
\theoremstyle{myexample}
\newtheorem{xexample}{Example}
\newenvironment{example}%
{\pushQED{\qed}\begin{xexample}}%
{\popQED\end{xexample}}
\newtheorem{xremark}{Remark}
\newenvironment{remark}%
{\pushQED{\qed}\begin{xremark}}%
{\popQED\end{xremark}}
\newtheoremstyle{exercise}{1em}{1em}{}{}{\scshape}{.}{1em}{}
\theoremstyle{exercise}
\newtheorem{exercise}{Exercise}
\newtheoremstyle{theorem}%
{1em}{1em}%
{\itshape}%
{}%
{\itshape\bfseries}%
{}%
{0pt}%
{\thmname{#1}\thmnumber{ #2}.\quad #3\\[4pt]}
\theoremstyle{theorem}
\newtheorem{theorem}{Theorem}
\usepackage{mathtools}
\usepackage{mdframed}
\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage{tikz}
\usetikzlibrary{automata,positioning}
\tikzset{>=stealth}
\tikzset{state/.append style={minimum size=15pt}}
\usepackage{relsize}
\usepackage{cleveref}
\usepackage{enumitem}
\usepackage{multicol}
\usepackage{stackengine}
\crefname{figure}{Figure}{Figures}
\crefname{xdefinition}{Definition}{Definitions}
\crefname{xexample}{Example}{Examples}
\crefname{xremark}{Remark}{Remarks}
\crefname{exercise}{Exercise}{Exercises}
\crefname{algorithm}{Algorithm}{Algorithms}
\usepackage[color]{changebar}
\newif\ifchangebar\changebarfalse
\let\oldcbend\cbend
\def\cbend{\oldcbend\changebarfalse}
\newcommand{\changechangebar}[2][2pt]{\ifchangebar\cbend\fi\cbcolor{#2}\cbstart[#1]\changebartrue}
\newcommand{\erin}{\changechangebar{yellow}}
\newcommand{\camil}{\changechangebar{red}}
\newcommand{\both}{\changechangebar[1pt]{orange}}
\renewcommand*{\arraystretch}{1.3}
\DeclareMathOperator{\defeq}{\overset{\text{def}}{=}}
\DeclareMathOperator{\Uop}{\mathbf{U}}
\DeclareMathOperator{\Wop}{\mathbf{W}}
\DeclareMathOperator{\Xop}{\raisebox{1pt}{$\bigcirc$}}
\DeclareMathOperator{\Fop}{\lozenge}
\DeclareMathOperator{\Gop}{\square}
\DeclareMathOperator{\Sop}{\mathbf{S}}
\DeclareMathOperator{\Pop}{\raisebox{1pt}{$\bigcirc$}^{--1}}
\let\vDash\models
\def\nvDash{\not\models}
\newcommand{\wff}{\emph{wff}} % Well-formed formula
\newcommand{\wffn}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{0}}} % Pure present wff
\newcommand{\wfff}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{$+$}}} % Pure future wff
\newcommand{\wffp}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{$-$}}} % Pure past wff
\title{Past Modalities in LTL}
\subtitle{Model Checking, Assignment 1}
\author{Camil Staps \and Erin van der Veen}
\begin{document}
\both
\maketitle
\setcounter{section}{5}
\setcounter{subsection}{2}
% The extra newlines are needed for correct changebars
\input{intro}
\input{syntax}
\input{semantics}
\input{equivalence}
\input{conversion}
\input{bad-prefix}
\input{summary}
\input{exercises}
\both
\printbibliography
\section*{Contribution}
Erin has started writing the text.
This text was then copy-edited, slightly corrected where needed and expanded by Camil.
(The result was then copy-edited, slightly corrected where needed and expanded by Erin.
The result was then copy-edited, slightly corrected where needed and expanded by Camil.)$^\omega$
In the above, yellow bars indicate content primarily contributed by Erin, whereas red bars indicate content primarily contributed by Camil.
They show that we both contributed to the core material, but also both specialised into one particular aspect:
Erin has figured out the translation of PLTL formulas to LTL via B\"uchi and Muller automata;
Camil has worked on the upper bound for bad prefixes of the form $vw^k$ when $vw^\omega$ is a counterexample for a safety property.
Thin orange bars indicate material that cannot be attributed to either.
Unfortunately, shortcomings of the \textsf{changebar} package make it impossible to indicate the fine-grainedness of our redaction process.
\cbend
\end{document}
|
