\documentclass[a4paper]{scrartcl}

\usepackage[backend=biber,natbib]{biblatex}
\bibliography{library}

\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}
\renewcommand{\qedsymbol}{$\blacksquare$}
\let\leq\leqslant
\let\le\leqslant
% 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}
\usepackage{mathtools}
\usepackage{mdframed}
\usepackage{tikz}
\usetikzlibrary{automata,positioning}
\usepackage{relsize}
\usepackage{parskip}
\usepackage{cleveref}
\usepackage{enumitem}
\usepackage{stackengine}
\crefname{figure}{Figure}{Figures}
\usepackage[color]{changebar}
\newif\ifchangebar\changebarfalse
\let\oldcbend\cbend
\def\cbend{\oldcbend\changebarfalse}
\newcommand{\erin}{\ifchangebar\cbend\fi\cbcolor{yellow}\cbstart\changebartrue}
\newcommand{\camil}{\ifchangebar\cbend\fi\cbcolor{red}\cbstart\changebartrue}

\renewcommand*{\arraystretch}{1.3}

\DeclareMathOperator{\defeq}{\overset{\text{def}}{=}}
\DeclareMathOperator{\Uop}{\mathbf{U}}
\DeclareMathOperator{\Wop}{\mathbf{W}}
\DeclareMathOperator{\Xop}{\bigcirc}
\DeclareMathOperator{\Fop}{\lozenge}
\DeclareMathOperator{\Gop}{\square}
\DeclareMathOperator{\Sop}{\mathbf{S}}
\DeclareMathOperator{\Pop}{\bigcirc^{--1}}

\title{Model Checking}
\subtitle{Assignment 1}
\author{Camil Staps \and Erin van der Veen}

\begin{document}

\maketitle

\setcounter{section}{5}
\setcounter{subsection}{2}

\subsection{Past Modalities in LTL}
% Explain that past Modalities are not necessary for a complete logic
% Explain that PLTL does make the logic more succinct (Paper 1)
%TODO: Give example on what kind of things we want to express with PLTL
\erin
As mentioned in Remark 5.16, LTL can be extended with \emph{past modalities}.
This section discusses this extension.
The combination of LTL and Past Modalities is often called \enquote{LTL-Past} or PLTL.
For the sake of brevity we will use the second (PLTL) 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.
Only later, when it was shown that past modalities do not increase the expressive power of LTL~\cite{Gabbay1980},
computing scientists stopped considering past modalities for reasons of minimality.

\erin
In 2003, Nicolas Markey showed that while past modalities do not increase expressive power,
they can make LTL formulas exponentially more succinct~\cite{Markey2003}.
In other words, there is a class of PLTL formulae%
	\footnote{In keeping with the style of the rest of the book, we alternate between \enquote{formulas} and \enquote{formulae} and wish the reader best of luck with this.}
	for which the size of all equivalent LTL formulas is $\Omega\left(2^n\right)$.
Markey achieves this proof by providing a formula that is in exactly this class.
Besides being smaller, PLTL formulas can also be easier to write and understand, as examples below will demonstrate.
They are also included in many model checking tools, such as NuSMV.
For this reason, it is useful to discuss them here.
\cbend

\subsubsection{Syntax}
% Provide formal syntax
% Provide intuitive semantics
%TODO: Provide formal semantics
\erin
This subsection describes the syntax of PLTL.
PLTL uses the same operators as LTL and adds two additional operators:
	$\Pop$ (pronounced \enquote{previously}) and
	$\Sop$ (pronounced \enquote{since}).
The $\Pop$-modality is comparable to $\Xop$.
Formula $\Pop\phi$ holds at some moment if $\phi$ held in the previous \enquote{step}.
The $\Sop$-modality is comparable to $\Uop$: $\phi_1\Sop\phi_2$ holds if $\phi_2$ held at some previous moment
	and $\phi_1$ held ever after that moment up to and including the current moment.

\begin{definition}[Syntax of PLTL]
	PLTL formulae over the set $AP$ of atomic propositions are formed according to the following grammar:
	\[
		\phi
			::=
			\left.\raisebox{0pt}[5pt][5pt]{} \text{true}
			\enspace\middle|\enspace a
			\enspace\middle|\enspace \phi_1 \land \phi_2
			\enspace\middle|\enspace \lnot \phi
			\enspace\middle|\enspace \bigcirc \phi
			\enspace\middle|\enspace \phi_1 \Uop \phi_2
			\enspace\middle|\enspace \Pop \phi
			\enspace\middle|\enspace \phi_1 \Sop \phi_2
			\right.
	\]
	where $a \in AP$.
\end{definition}

\camil
The precedence order of the operators borrowed from LTL remains the same.
$\Pop$ binds equally strong as $\Xop$ and $\lnot$.
$\Sop$ takes precedence over $\Uop$, and like $\Uop$ is right-associative.

As with LTL, we can also derive additional operators in PLTL.
They can be seen as counterparts of the derived LTL modalities $\square$ and $\lozenge$:
	$\square^{-1}$ (\enquote{was always}, since the beginning until now) and
	$\lozenge^{-1}$ (\enquote{was sometime}, now or at some point before now).

\erin
\begin{definition}[Derived PLTL operators]
	Given $\phi \in PLTL$, then:
	\begin{equation*}
			\Fop^{-1} \phi \defeq \top \Sop \phi \qquad
			\Gop^{-1} \phi \defeq \neg \Fop^{-1} \neg \phi
		\qedhere
	\end{equation*}
\end{definition}

Their intuitive meaning is as follows.
$\Fop^{-1} \phi$ ensures that at some point in the past $\phi$ was true.
$\Gop^{-1} \phi$ is satisfied when there is no moment in the past on which $\phi$ did not hold.
In other words, $\Gop^{-1}$ entails that $\phi$ held globally until this point.

\Cref{fig:PLTL_intuitive} shows the intuitive meanings of the past modalities for the simple case where $a$ and $b$ are the only atomic propositions.
The left hand side of the figure shows some PLTL formulae;
the right hand side shows sequences for which this formula holds.
Since we need to also consider the past,
we include an arrow that points to the state for which the formula holds.

\begin{figure}
	\tikzset{intuitive semantics/.style={shorten >=1pt,node distance=16mm,on grid,initial text={},baseline=-0.5ex,->}}
	\tikzset{state/.append style={minimum size=15pt}}
	\tikzset{arbitrary/.style={state,label={[font=\relsize{-2}]arbitrary}}}
	\centering
	\[\begin{array}{rcl}
	\text{since} & a \Sop b &
	\begin{tikzpicture}[intuitive semantics]
		\node                                (0)              {\dots};
		\node[arbitrary]                     (1) [right of=0] {};
		\node[state,label=$b$]               (2) [right of=1] {};
		\node[state,label=$a$]               (3) [right of=2] {};
		\node[state,label=$a$,initial below] (4) [right of=3] {};
		\node[arbitrary]                     (5) [right of=4] {};
		\node                                (6) [right of=5] {\dots};
		\path (0) edge (1)(1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6);
	\end{tikzpicture}\\
	\text{previously} & \Pop a &
	\begin{tikzpicture}[intuitive semantics]
		\node                          (0)              {\dots};
		\node[arbitrary]               (1) [right of=0] {};
		\node[arbitrary]               (2) [right of=1] {};
		\node[state,label=$a$]         (3) [right of=2] {};
		\node[arbitrary,initial below] (4) [right of=3] {};
		\node[arbitrary]               (5) [right of=4] {};
		\node                          (6) [right of=5] {\dots};
		\path (0) edge (1)(1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6);
	\end{tikzpicture}\\
	\text{was sometime} & \Fop^{-1} a &
	\begin{tikzpicture}[intuitive semantics]
		\node                          (0)              {\dots};
		\node[arbitrary]               (1) [right of=0] {};
		\node[state,label=$a$]         (2) [right of=1] {};
		\node[arbitrary]               (3) [right of=2] {};
		\node[arbitrary,initial below] (4) [right of=3] {};
		\node[arbitrary]               (5) [right of=4] {};
		\node                          (6) [right of=5] {\dots};
		\path (0) edge (1)(1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6);
	\end{tikzpicture}\\
	\text{was always} & \Gop^{-1} a &
	\begin{tikzpicture}[intuitive semantics]
		\node                                (0)              {\dots};
		\node[state,label=$a$]               (1) [right of=0] {};
		\node[state,label=$a$]               (2) [right of=1] {};
		\node[state,label=$a$]               (3) [right of=2] {};
		\node[state,label=$a$,initial below] (4) [right of=3] {};
		\node[arbitrary]                     (5) [right of=4] {};
		\node                                (6) [right of=5] {\dots};
		\path (0) edge (1)(1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6);
	\end{tikzpicture}
	\end{array}\]
	\caption{Intuitive semantics of past modalities.}
	\label{fig:PLTL_intuitive}
\end{figure}

\camil
Dual modalities, like the LTL $\square\lozenge$ \enquote{infinitely often} and \enquote{eventually forever}, are less useful in PLTL.
$\square^{-1}\lozenge^{-1}\phi$ intuitively holds when at every point in the past, $\phi$ held or there was a previous moment at which $\phi$ held.
This is satisfied precisely when $\phi$ held at the first moment in time.
Interestingly, $\lozenge^{-1}\square^{-1}\phi$ means the same: it holds when $\phi$ held from the beginning until some moment in the past.
The reason that dual modalities in PLTL are less useful is that we still consider traces with a fixed starting point.
Thus, while with future modalities it is possible to look infinitely far in the future, it is not possible to look infinitely far in the past.

%TODO: Give examples of semantics along the lines of subsection 5.1.1.
Before turning to the formal semantics in the next subsection, we provide some examples.

\begin{example}[Properties for a Traffic Light]
	We return to the traffic light of Example 5.4.
	Since dual past modalities are less useful than dual future modalities, we cannot express the liveness property $\square\lozenge\textsl{green}$ with a pure past formula.
	However, the requirement \enquote{once red, the light cannot become green immediately} \emph{can} be expressed with past modalities.
	To rewrite it, consider that this requirements is equivalent to \enquote{if green, the light cannot have been red previously}.
	This yields the formula:
	\[\square\left(\textsl{green} \rightarrow \lnot \Pop\textsl{red}\right) \qedhere\]
\end{example}

\begin{example}[Properties for an Authentication System]
	\citet{FiterauBrostean2017} use past modalities to describe properties of the Secure Shell (SSH) protocol.
	One property says that if a channel is opened, there must have been some successful authentication attempt in the past~\citep[p.~149]{FiterauBrostean2017}.
	Also, since that successful authentication, no authentication failure must have occurred.
	This formula is intuitively expressed by $\square(\textsl{hasOpenedChannel} \rightarrow \lnot \textsl{authFailure} \Sop \textsl{authSuccess})$.
	Expressing this property in LTL is obscure and tedious.
	One way uses the Weak Until operator from Section 5.1.5:
	%TODO please check that this is actually equivalent
	\begin{align*}
		& \lnot \textsl{hasOpenedChannel} \Wop\\
		& \quad (\textsl{authSuccess} \land (\square \textsl{authFailure} \rightarrow \lnot \textsl{hasOpenedChannel} \Uop \textsl{authSuccess}))
		\qedhere
	\end{align*}
\end{example}
\cbend

\subsubsection{Semantics}
\erin
The semantics of LTL and PLTL are defined in a very similar way.
However, we must make some modifications to the definitions.
\camil
In particular, the $\vDash$ operator must be redefined.
Recall that for LTL we wrote $\sigma \vDash \phi$ when $\sigma$ satisfies $\phi$ and $\sigma[i\dots]$ for the suffix of $\sigma$ starting in the $(j+1)$st symbol.
The latter notation effectively loses information about the prefix.
In the case of PLTL, we cannot lose this information.
For this reason, we use a satisfaction relation at a specific index.
We will write this as $\sigma \vDash_i \phi$, read as \enquote{$\sigma$ satisfies $\phi$ at $i$}.%
\footnote{%
	The notation used in literature varies.
	\citet{Lichtenstein1985} use $(\sigma,i) \vDash \phi$; \citet{Markey2003} uses $\sigma,i \vDash \phi$.
	Although the difference is minor, we find $\vDash_i$ more intuitive because it shows that the object being checked is the same in $\sigma\vDash_i\phi$ and $\sigma\vDash_j\phi$.}
We use $\sigma \vDash \phi$ as a shorthand for $\sigma \vDash_0 \phi$.

\erin
\begin{definition}[Semantics of PLTL (Interpretation over Words)]
	Let $\phi$ be a PLTL formula over $AP$. The LT property induced by $\phi$ is
	\[Words(\phi) = \{\sigma \in \left(2^{AP}\right)^\omega \mid \sigma \vDash \phi\}\]
	where $\vDash\ \subseteq \left(2^{AP}\right)^\omega \times \mathbb{N} \times PLTL$ is the smallest relation with the properties in \cref{fig:PLTL-semantics}.
\end{definition}
\camil
Note that we must redefine the satisfaction relation for the LTL operators, because $\vDash$ is now a ternary relation.
The difference with LTL formulae is well illustrated by the $\bigcirc$ operator.
In the LTL case, $\sigma=A_0A_1A_2\dots\vDash\bigcirc\phi$ iff $\sigma[1\dots]=A_1A_2\dots\vDash\phi$.
Thus, whether $\bigcirc\phi$ holds for $\sigma$ cannot depend on $A_0$.
In the PLTL case, $\sigma\vDash_i\bigcirc\phi$ iff $\sigma\vDash_{i+1}\phi$.
The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\sigma$ may depend on $A_0$,
	as is trivially the case with $\bigcirc\bigcirc^{-1}a$.

\begin{figure}
	\centering
	\begin{mdframed}
	\[
		\begin{matrix*}[l]
			\sigma &\vDash_i & \text{true}\\
			\sigma &\vDash_i & a                 &\text{iff} & a\in A_i\\
			\sigma &\vDash_i & \phi_1\land\phi_2 &\text{iff} & \text{$\sigma\vDash_i\phi_1$ and $\sigma\vDash_i\phi_2$}\\
			\sigma &\vDash_i & \lnot\phi         &\text{iff} & \sigma \nvDash_i \phi\\
			\sigma &\vDash_i & \bigcirc\phi      &\text{iff} & \sigma \vDash_{i+1} \phi\\
			\sigma &\vDash_i & \phi_1\Uop\phi_2  &\text{iff} & \exists_{j \le 0}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_i \phi_1$ for all $0 \le i < j$}\\
			\sigma &\vDash_i & \phi_1\Sop\phi_2  &\text{iff} & \exists_{j \le i}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_k \phi_1$ for all $j < k \le i$}\\
			\sigma &\vDash_i & \Pop\phi          &\text{iff} & i \geq 1 \wedge \sigma \vDash_{i-1} \phi
		\end{matrix*}
	\]
	\end{mdframed}
	\caption{PLTL semantics for infinite words $\sigma=A_0A_1A_2\dots \in \left(2^{AP}\right)^\omega$.}
	\label{fig:PLTL-semantics}
\end{figure}

\erin
\begin{definition}[Semantics of PLTL over Paths and States]
	Let $TS = (S, Act, \rightarrow, I, AP, L)$ be a transition system without terminal states, and let $\phi$ be an PLTL-formula over AP.
	\begin{itemize}
		\item For infinite path fragments $\pi$ of $TS$, the satisfaction relation is defined by
			\[\pi \vDash \phi \Leftrightarrow trace(\pi) \vDash \phi\]
		\item For state $s \in S$, the satisfaction relation $\vDash$ is defined by
			\[s \vDash \phi \Leftrightarrow \forall_{\pi \in Paths(s)}[\pi \vDash \phi]\]
			\item $TS$ satisfies $\phi$, denoted by $TS \vDash \phi$ if $Traces \vDash \phi$, if $Traces(TS) \subseteq Words(\phi)$
				\qedhere
	\end{itemize}
\end{definition}
In order to make these definitions suitable for use with our PLTL operators,
we must provide their semantics.
\Cref{fig:PLTL-semantics} shows the formal semantics of the operators defined in the grammar.
Note that we need to add a index $i$, since we must also be able to look in the past.

Given these definitions, it is possible to derive the formal semantics of the $\Fop^{-1}$ and $\Gop^{-1}$ operators as well:
\[
	\begin{matrix*}[l]
		\sigma &\vDash_i &\Fop^{-1}\phi &\text{iff} &\exists_{k \leq i}[\sigma \vDash_k \phi]\\
		\sigma &\vDash_i &\Gop^{-1}\phi &\text{iff} &\forall_{k \leq i}[\sigma \vDash_k \phi]
	\end{matrix*}
\]

\subsubsection{Specifying Properties}
% TODO Once operator

\camil
\begin{remark}[Other Notations]
	% TODO: I don't find this place logical for this remark, but it is the same place as Remark 5.16 in the book.
	Like for LTL, many different notations are used in literature for PLTL.
	These include
		$\mathbf X^{-1}, \mathbf G^{-1}, \mathbf F^{-1}$~\citep[e.g.]{Markey2003},
		but also \raisebox{-1pt}{\tikz\draw[black,fill=black](0,0)circle(.4em);}$,\blacksquare,\blacklozenge$~\citep[e.g.]{Gabbay1989}
		or $\stackinset{c}{}{c}{}{$\cdot$}{$\bigcirc$},\boxdot,\stackinset{c}{}{c}{}{$\cdot$}{$\lozenge$}$~\citep[e.g.]{Havelund2002}.
	% It is always fun to come up with new versions and watch people struggling to reproduce them in \LaTeX.
\end{remark}

\erin
\subsubsection{Equivalence of PLTL Formulae}
Now that we have defined the formal semantics of PLTL,
we can define equivalence on PLTL formulas.

\begin{definition}[Equivalence of PLTL Formulae]
	PLTL formulae $\phi_1,\phi_2$ are equivalent, denoted $\phi_1 \equiv \phi_2$ iff they verify the following property:
	\[\text{for any path } \pi \text{ and any position } i, \pi \vDash_i \phi \Leftrightarrow \pi \vDash_i \psi \qedhere\]
\end{definition}

Additionally, we can define another form of equivalence, initial equivalence:
\begin{definition}[Initial Equivalence of PLTL Formulae]
	PLTL formulae $\phi_1,\phi_2$ are initially equivalent, denoted $\phi_1 \equiv_0 \phi_2$ iff they verify the following property:
	\[\text{for any path } \pi, \pi \vDash_0 \phi \Leftrightarrow \pi \vDash_0 \psi \qedhere\]
\end{definition}
\cbend

\subsubsection{LTL and PLTL}
%TODO: Consider/Analyse differences between LTL and PLTL

\subsubsection{PLTL to LTL}
%TODO: Provide the syntactic algorithm to convert PLTL to LTL
%TODO: Provide algorithm via automata to convert PLTL to LTL
%TODO: In both cases make use of examples from SSH Paper

%TODO: (Section?) Assess if PLTL is actually more succinct using the examples from the SSH Paper

\subsubsection{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?

\subsection{Summary}
% TODO: points to be added to 5.3

\subsection{Bibliographic Notes}
% TODO: points to be added to 5.4
% A possibly helpful list is at https://cstheory.stackexchange.com/a/29452
% Also the bibliography file should be worked through.

\subsection{Exercises}
% After the exam documentclass; http://compgroups.net/comp.text.tex/-if-else-fi-in-new-environment/263869
\newif\ifshowanswers\showanswerstrue
\newenvironment{answer}%
	{\ifshowanswers\par\bgroup\small\textit{Answer:}\else\setbox0\vbox\bgroup\fi}%
	{\egroup}
\newcommand{\hint}[1]{\par\textit{Hint: #1}}
\camil
\begin{exercise}
	In this exercise we prove that PLTL formulas can be exponentially more succinct.
	The proof followed here is that of \citet{Markey2003} which, in turn, is based on work by \citet{Etessami2002}.
	The proof is achieved by giving an example of a formula which can be expressed in $\mathcal O(n)$ in PLTL but requires $\Omega(n)$ in LTL.

	Take $n\in\mathbb N$ and $AP=\{p_0,\dots,p_n\}$.
	We first show that there is no polynomial-size LTL formula expressing property~\ref{ex:proof-markey:prop-agreement}.
	\begin{equation}
		\phi_n(\sigma) \defeq
			\forall_{i,j\in\mathbb N}
			\left[
				\forall_{k\in[1,n]}
				[(A_i\vDash p_k) \Leftrightarrow (A_j\vDash p_k)]
				\rightarrow
				((A_i\vDash p_0) \Leftrightarrow (A_j\vDash p_0))
			\right]
		\label{ex:proof-markey:prop-agreement}
	\end{equation}
	where $\sigma=A_0A_1A_2\dots$.
	In other words, if two points on path $\sigma$ agree on $p_k$ for all $k\in[1,n]$, the points must also agree on $p_0$.

	\begin{enumerate}[label=(\alph*)]
		\item Find an $\mathcal O\left(2^n\right)$ LTL formula expressing property~\ref{ex:proof-markey:prop-agreement}.
			\hint{if the formula can be $\mathcal O\left(2^n\right)$, what are you allowed to quantify over?}
			\begin{answer}%
				\footnote{Note that this is slightly different from the version in \citet[p. 4]{Markey2003}.
					The limit on the leftmost $\wedge$ has $i\in[1,n]$ rather than $i\in[0,n]$ in the original paper.
					We believe this to be an error, because otherwise $a_0$ is a free variable.} %TODO do you agree?
				\[\phi_n(\sigma) =
					\bigwedge_{\substack{a_i\in\{\top,\bot\}\\i\in[0,n]}} \left[
						\left(\lozenge(\bigwedge\nolimits_{i=0}^n p_i=a_i)\right)
						\rightarrow
						\square\left((\bigwedge\nolimits_{i=1}^n p_i=a_i) \rightarrow p_0=a_0\right)
					\right]
				\]
			\end{answer}

		\item Assume a polynomial-size LTL formula exists for property~\ref{ex:proof-markey:prop-agreement}.
			What can you say of the size of a B\"uchi automaton $\mathcal A$ recognizing $\textsl{Words}(\phi_n)$?
			\label{ex:proof-markey:assumption}
			\hint{consider Theorem 5.41.}
			\begin{answer}
				There exists a B\"uchi automaton of size $\mathcal O(2^{n^k})$ for some $k\in\mathbb N$.
			\end{answer}

		\item Let $A=a_0,\dots,a_{2^n-1}$ be any permutation of $2^{AP\setminus\{p_0\}}$.
			Define $w_K=b_{K,0}\dots b_{K,2^n-1}$ with
			\[
				b_{K,i} \defeq
				\begin{cases}
					a_i              & \text{iff $i\notin K$}\\
					a_i \cup \{p_0\} & \text{iff $i\in K$.}
				\end{cases}
			\]
			Show that if $K,K' \subseteq \{0,\dots,2^n-1\}$ and $K\ne K'$, also $w_K \ne w_{K'}$.
			\label{ex:proof-markey:different-w_K}
			\begin{answer}
				Without loss of generality, assume there exists an $i\in K$ with $i\notin K'$.
				Then $p_0\in b_{K,i}$ but $p_0\notin b_{K',i}$.
				Hence, $w_K\ne w_{K'}$.
			\end{answer}

		\item How many distinct words $w_K$ exist?
			\label{ex:proof-markey:nr-of-w_k}
			\begin{answer}
				There are $2^{|\{0,\dots,2^n-1\}|} = 2^{2^n}$ distinct $K$ (and equally many distinct $w_K$).
			\end{answer}

		\item Show that $w_K^\omega$ is accepted by $\mathcal A$.
			\begin{answer}
				Since all $a_i$ are distinct,
					two points $b_{K,j}, b_{K,k}$ on $w_K^\omega$ agree on all $p_i$ for $i\in[1,n]$ iff $j\equiv k \pmod{2^n}$.
				In this case, they also agree on $p_0$.
			\end{answer}

		\item It follows that there are paths $\pi_K$ and $\pi_{K'}$ in $\mathcal A$ accepting $w_K^\omega$ and $w_{K'}^\omega$ respectively.
			Let $q_K$ and $q_{K'}$ be the $2^n$-th states of each of these paths.
			Assume that $q_K = q_{K'}$.
			Construct from $w_K$ and $w_{K'}$ an infinite word $v$ that is accepted by $\mathcal A$ but does not satisfy $\phi_n$.
			\hint{take the simplest infinite word using both words that you can think of.}
			\begin{answer}
				Take $v=w_Kw_{K'}^\omega$.
				Apart from the prefix of size $2^n$, the path of this word is equal to that of $w_{K'}^\omega$, which is accepted.
				So $v$ is accepted.
				From \ref{ex:proof-markey:different-w_K} we have an $i$ such that $p_0\in b_{K,i}$ but $p_0\notin b_{K',i}$.
				However, for all $i\in[1,n]$, $p_i\in b_{K,i} \Leftrightarrow p_i\in b_{K',i}$.
				Therefore, $i=i, j=i+2^n$ is a counterexample to the outermost quantifier of $\phi_n$.
			\end{answer}

		\item Show that this contradicts the assumption from \ref{ex:proof-markey:assumption}.
			\begin{answer}
				Since we have $2^{2^n}$ distinct $w_K$ [cf. \ref{ex:proof-markey:nr-of-w_k}] and the $2^n$-th states of their accepting paths must all be distinct,
					$\mathcal A$ has at least $2^{2^n}$ states.
					But $2^{2^n} \notin \mathcal O(2^{n^k})$.
			\end{answer}

		\item We now turn to a slightly different property:
			\begin{equation}
				\psi_n(\sigma) \defeq
					\forall_{i\in\mathbb N}
					\left[
						\forall_{k\in[1,n]}
						[(A_i\vDash p_k) \Leftrightarrow (A_0\vDash p_k)]
						\rightarrow
						((A_i\vDash p_0) \Leftrightarrow (A_0\vDash p_0))
					\right]
				\label{ex:proof-markey:prop-agreement-2}
			\end{equation}
			Property \ref{ex:proof-markey:prop-agreement-2} holds if all points on $\sigma$ that agree with all $p_k$ for $k\in[1,n]$ with $A_n$ also agree on $p_0$.
			Give an $\mathcal O(n)$ PLTL formula expressing property \ref{ex:proof-markey:prop-agreement-2}.
			\hint{recall the semantics of the dual modalities in PLTL.}
			\begin{answer}
				\[\psi_n(\sigma) =
					\square\left[
						\left(\bigwedge\nolimits_{i=1}^n (p_i \Leftrightarrow \lozenge^{-1}\square^{-1}p_i)\right)
						\Rightarrow
						(p_0 \Leftrightarrow \lozenge^{-1}\square^{-1}p_0)
					\right]
				\]
			\end{answer}

		\item Construct an LTL formula for $\phi_n$ using the PLTL formula for $\psi_n$ and conclude the proof.
			\hint{first construct an LTL formula for $\psi_n$.}
			\begin{answer}
				Take $\phi'_n \defeq \square\psi'_n$, where $\psi'_n$ is an LTL formula initially equivalent to $\psi_n$.
				By virtue of the $\square$ operator, $\phi_n\equiv\phi'_n$.
				But $\phi_n$ is $\mathcal O(2^n$, so also $\phi'_n$ is exponential.
				Since $\phi'_n$ is $\mathcal O(2^n)$ and $\psi_n$ is $\mathcal O(n)$,
					the PLTL formula for property~\ref{ex:proof-markey:prop-agreement-2} is exponentially more succinct than the LTL formula.
				\qed
			\end{answer}
	\end{enumerate}
\end{exercise}
\cbend

\printbibliography

\section*{Contribution}
%TODO: Like we are some immature group of children, we have to provide proof of contribution
\camil
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.
Unfortunately, disabilities of the \textsf{changebar} package make it impossible to indicate the fine-grainedness of our redaction process.
\cbend

\end{document}