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