\documentclass[10pt,a4paper]{article}

\usepackage{geometry}
\usepackage[english]{babel}

\usepackage{enumitem}
\setenumerate[1]{label=\alph*)}

\usepackage{fancyhdr}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}
\fancyhead{}
\fancyfoot[C]{Copyright {\textcopyright} 2016 Camil Staps}
\pagestyle{fancy}

\usepackage{sv}

\title{Software Verification - assignment 1}
\author{Camil Staps}

\begin{document}

\maketitle
\thispagestyle{fancy}

\setcounter{section}{2}
\section{Expressing the ABP in LTL}

\begin{enumerate}
    \item $\always(\lnot(A_{S0}\land A_{S1}))$.
    \item $\always(A_{S0}\lor A_{S1})$.
    \item $\always\eventually(A_{S0}\lor A_{S1})$.
    \item $\always(A_{Sb}\then\eventually B_{Sb})$, $b\in\{0,1\}$.
    \item $\always(A_{Sb}\then\next B_{Rb})$, $b\in\{0,1\}$.
    \item $\always(B_{R0}\then B_{S0}\until B_{R1})$.
    \item $\always(A_{S0}\then \lnot A_{S1}\until A_{R0})$.
    \item Cannot be expressed: there are no atomic propositions defined for `$A$ can send'.
    \item $\always(A_{Sb}\then(\eventually B_{Rb})\lor(\always\lnot B_{Rb}))$, $b\in\{0,1\}$. However, this is rather silly, since $\always((\eventually p)\lor(\always\lnot p))$ always holds.
\end{enumerate}

\end{document}

