Lalala

6 files changed, 35 insertions, 23 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index cb1b363..e859f41 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -99,8 +99,8 @@
 \newcommand{\wfff}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{$+$}}} % Pure future wff
 \newcommand{\wffp}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{$-$}}} % Pure past wff
 
-\title{Model Checking}
-\subtitle{Assignment 1}
+\title{Past Modalities in LTL}
+\subtitle{Model Checking, Assignment 1}
 \author{Camil Staps \and Erin van der Veen}
 
 \begin{document}
@@ -116,25 +116,22 @@
 \input{semantics}
 \input{equivalence}
 \input{conversion}
-%TODO: (Section?) Assess if PLTL is actually more succinct using the examples from the SSH Paper
 \input{bad-prefix}
 
 \input{summary}
-\input{bibliographic-notes}
 \input{exercises}
 
 \both
 \printbibliography
 
 \section*{Contribution}
-%TODO: Like we are some immature group of children, we have to provide proof of 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.
 Thin orange bars indicate material that cannot be attributed to either.
-Unfortunately, disabilities of the \textsf{changebar} package make it impossible to indicate the fine-grainedness of our redaction process.
+Unfortunately, shortcomings of the \textsf{changebar} package make it impossible to indicate the fine-grainedness of our redaction process.
 \cbend
 
 \end{document}
diff --git a/Assignment1/bibliographic-notes.tex b/Assignment1/bibliographic-notes.tex
deleted file mode 100644
index e5d7f3a..0000000
--- a/Assignment1/bibliographic-notes.tex
+++ /dev/null
@@ -1,5 +0,0 @@
-\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.
-\emph{NB: these notes are to be added to the current section 5.4.}
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 8919366..5b97530 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -299,13 +299,13 @@ After all, these formulas are meaningless for $\vDash_0$, since (using Gabbay's
 The Automata-based Algorithm, which we will call the semantic algorithm henceforth, is based on the following translations:
 \begin{enumerate}
 	\item PLTL formulas can be converted to B\"uchi automata~\cite{Lichtenstein1985}
-	\item B\"uchi automata can be converted to deterministic Muller automata
+	\item B\"uchi automata can be converted to deterministic Muller automata~\citep{Safra1988}
 	\item Muller automata can be converted to LTL formulae~\cites{Maler1990, Maler1994}
 \end{enumerate}
 
-Converting an LTL formula to a B\"uchi automata is discussed in Section 5.2 of this book.
+Converting an LTL formula to a B\"uchi automaton is discussed in Section 5.2 of this book.
 Much of this algorithm is the same,
-we must just modify some figures and definitions in order to be able to apply it on PLTL formulae.
+we only need to modify some figures and definitions in order to be able to apply it on PLTL formulae.
 The first Definition we must change is 5.35:
 \begin{definition}[Elementary Sets of PLTL Formulas]
 	$B \subseteq closure(\phi)$ is \emph{elementary} if it is consistent with respect to propositional logic, maximal, and locally consistent with respect to the until and since operators.
@@ -376,29 +376,28 @@ Let us first define the Muller Automaton:
 Converting NBAs to Muller automata was shown to be possible by \citet{McNaughton1966}
 and is part of what is known as McNaughton's theorem.
 There are multiple ways to convert a NBA to a Muller Automaton.
-In this book we will describe Safra's Determinization Algorithm.
+In this book we will describe Safra's Determinization Algorithm~\citep{Safra1988}.
 
-%TODO: Safra's algorithm might be used directly?
 Safra's algorithm is an algorithm based on subset construction that is capable of determinizing non-deterministic B\"uchi automata.
 In this book, we will not describe the underlying theory of the algorithm.
 Instead, we will provide you with a simple description.
 A more thorough look into the algorithm can be found in a book by Markus Roggenbach~\cite{Roggenbach2002}.
 We will follow mostly the same description as provided by Roggenbach, with slight modifications.
 
-Let $B = (\mathcal{Q}, \Sigma, q_0, \Delta, F)$ be a NBA.
-Safra's algorithm returns an automata without accepting condition where the states are constructed as trees of $\mathcal{Q}$.
+Let $B = (Q, \Sigma, q_0, \delta, F)$ be a NBA.
+Safra's algorithm returns an automata without accepting condition where the states are constructed as trees of $Q$.
 Once this automaton is returned,
 an accepting condition must be chosen.
 Given that we want to construct a Muller Automaton,
 we create a set of sets of states containing trees.
-For the purpose of this book, Safra's algorithm will therefore be considered to return a Muller Automaton $A = (\mathcal{Q}', \Sigma, q_0', \delta, F')$.
+For the purpose of this book, Safra's algorithm will therefore be considered to return a Muller Automaton $A = (Q', \Sigma, q_0', \delta', F')$.
 
-Choose $V := \{1, 2, \dots, 2|\mathcal{Q}|\}$ for denoting nodes in Safra trees.
+Choose $V := \{1, 2, \dots, 2\cdot|Q|\}$ for denoting nodes in Safra trees.
 
 \begin{enumerate}
 	\item $q_0'$ is the Safra tree\footnote{Safra trees are defined in Roggenbachs book.} consisting of node 1 labelled with macrostate $\{q_0\}$.
 	\item For every input $a$ and tree $T$ with set $N$ of nodes,
-		the value of the transition function $\delta(T,a)$ is computed as follows:
+		the value of the transition function $\delta'(T,a)$ is computed as follows:
 		\begin{enumerate}
 			\item Remove all marks ``!'' in $T$
 			\item For every node $v$ with macrostate $M$ such that $M \cap F \neq \emptyset$, create a new node $v' \in (V\\N)$, such that $v'$ becomes the youngest son of $v$ and carries the macrostate $M \cap F$.
@@ -410,7 +409,7 @@ Choose $V := \{1, 2, \dots, 2|\mathcal{Q}|\}$ for denoting nodes in Safra trees.
 	\item Prune all unreachable states.
 	\item Create $F'$ such that for every subset $S$ of $Q'$ it holds that for some $v \in V$:
 		\[
-			S \in F' \Leftrightarrow (\forall_{\text{Tree } t \in S} v \text{ is in } t) \wedge (\exists_{\text{Tree } t \in S} v \text{ is marked in } t)
+			S \in F' \Leftrightarrow (\forall_{\text{Tree } t \in S} v \text{ is in } t) \wedge \exists_{\text{Tree } t \in S} (v \text{ is marked in } t)
 		\]
 \end{enumerate}
 
diff --git a/Assignment1/exercises.tex b/Assignment1/exercises.tex
index ba056d5..930119b 100644
--- a/Assignment1/exercises.tex
+++ b/Assignment1/exercises.tex
@@ -91,7 +91,7 @@
 			\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?
+					We believe this to be an error, because otherwise $a_0$ is a free variable.}
 				\[\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)
diff --git a/Assignment1/library.bib b/Assignment1/library.bib
index 5f9fbcb..2035c70 100755
--- a/Assignment1/library.bib
+++ b/Assignment1/library.bib
@@ -159,3 +159,11 @@
 	year      = 2003,
 	pages     = {74--88}
 }
+
+@inproceedings{Safra1988,
+	author    = {Safra, S.},
+	title     = {On The Complexity of $\omega$-Automata},
+	booktitle = {29th Annual Symposium on Foundations of Computer Science},
+	pages     = {319--327},
+	year      = 1988
+}
diff --git a/Assignment1/summary.tex b/Assignment1/summary.tex
index d18e517..31b65f8 100644
--- a/Assignment1/summary.tex
+++ b/Assignment1/summary.tex
@@ -11,5 +11,18 @@
 		Because PLTL formulas need to be able to \enquote{look back}, the satisfaction relation $\vDash$ becomes ternary:
 			it is a subset of $\left(2^{AP}\right)^\omega \times \mathbb N \times PLTL$,
 			where the natural number indicates the index at which a trace satisfies a formula.
+
+	\item
+		For PLTL, there are two different notions of equivalence.
+		Initial equivalence $\phi \equiv_0 \psi$ means that all paths that satisfy $\phi$ in position 0 must also satisfy $\psi$ in position 0 (and vice versa).
+		Equivalence $\phi \equiv \psi$ means that for all paths $\pi$ and positions $i$, $\pi \vDash_i \phi$ entails $\pi \vDash_i \psi$ (and vice versa).
+
+	\item
+		Because past modalities do not increase expressiveness, PLTL formulas can be translated into initially equivalent LTL formulas.
+		This can be done with syntactic rewrite rules or with a conversion through B\"uchi automata and Muller automata.
+
+	\item
+		If $vw^\omega$ is a counterexample for a safety property $P$ in a finite transition system $TS$, there exists a $j \le |TS|\cdot2^{|\lnot P|}\cdot|\lnot P|$ for which $vw^j$ is a bad prefix for $P$.
+		However, in most cases a smaller counterexample (not of the form $vw^k$) can be found by translating $P$ to a finite automaton and running it with $vw^\omega$.
 \end{itemize}
 \cbend