Start with minimal bad prefixes

8 files changed, 32 insertions, 7 deletions

diff --git a/Assignment1/bad-prefix.tex b/Assignment1/bad-prefix.tex
index 98e39ed..a1db684 100644
--- a/Assignment1/bad-prefix.tex
+++ b/Assignment1/bad-prefix.tex
@@ -1,2 +1,14 @@
-\subsubsection{Minimal Bad Prefix in NuSMV}
+\camil
+\subsection{Minimal Bad Prefices}
 %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?
+\emph{NB: this section is not particularly about PLTL. It is better added as 5.1.7 or 5.2.3.}
+
+Model checking tools, such as NuSMV, often give counterexamples in the form of $vw^\omega$, i.e., a finite prefix with a infinite loop.
+In the case of safety properties, it is usually much more informative to give a counterexample in the form of a bad prefix~\citep[p.~293]{Kupferman2001}:
+	a finite path $v$ such that all paths with $v$ as prefix are counterexamples.
+
+Suppose an automaton $M$ violates safety property $S$ with the counterexample $vw^\omega$.
+In this case, we know that $vw^{|M|-1}$ is a bad prefix (where $|M|$ is the number of states of $M$).
+To see why, consider the visited states at positions $|v|, |v|+|w|, |v|+2\cdot|w|$, etc.
+These are the states visited at the beginning of the loop.
+\cbend
diff --git a/Assignment1/bibliographic-notes.tex b/Assignment1/bibliographic-notes.tex
index f4e9cd4..e5d7f3a 100644
--- a/Assignment1/bibliographic-notes.tex
+++ b/Assignment1/bibliographic-notes.tex
@@ -2,3 +2,4 @@
 % 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/exercises.tex b/Assignment1/exercises.tex
index 5849c84..647755e 100644
--- a/Assignment1/exercises.tex
+++ b/Assignment1/exercises.tex
@@ -1,4 +1,6 @@
+\camil
 \subsection{Exercises}
+\emph{NB: these exercises are to be added to the current section 5.5.}
 % After the exam documentclass; http://compgroups.net/comp.text.tex/-if-else-fi-in-new-environment/263869
 \newif\ifshowanswers\showanswerstrue
 \newenvironment{answer}%
@@ -6,7 +8,6 @@
 	{\egroup}
 \newcommand{\hint}[1]{\par\textit{Hint: #1}}
 
-\camil
 \begin{exercise}
 	For the PLTL formulas over $AP=\{a,b\}$ given below, determine whether they are \wffn, \wffp, \wfff\ or neither.
 
diff --git a/Assignment1/intro.tex b/Assignment1/intro.tex
index 6df3700..d07be86 100644
--- a/Assignment1/intro.tex
+++ b/Assignment1/intro.tex
@@ -21,6 +21,6 @@ In other words, there is a class of PLTL formulae%
 	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.
+They are also included in many model checking tools, such as NuSMV.%
+	\footnote{\url{http://nusmv.fbk.eu/}}
 For this reason, it is useful to discuss them here.
-\cbend
diff --git a/Assignment1/library.bib b/Assignment1/library.bib
index fdd6dfd..6555f23 100755
--- a/Assignment1/library.bib
+++ b/Assignment1/library.bib
@@ -120,3 +120,13 @@
 	year      = 1985,
 	pages     = {733--749}
 }
+
+@article{Kupferman2001,
+	author    = {Kupferman, Orna and Vardi, Moshe Y.},
+	title     = {Model Checking of Safety Properties},
+	journal   = {Formal Methods in System Design},
+	volume    = 19,
+	issue     = 3,
+	year      = 2001,
+	pages     = {291--314}
+}
diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex
index a48e163..7840cef 100644
--- a/Assignment1/semantics.tex
+++ b/Assignment1/semantics.tex
@@ -1,5 +1,5 @@
-\subsubsection{Semantics}
 \erin
+\subsubsection{Semantics}
 The semantics of LTL and PLTL are defined in a very similar way.
 However, we must make some modifications to the definitions.
 \camil
diff --git a/Assignment1/summary.tex b/Assignment1/summary.tex
index a888df8..d18e517 100644
--- a/Assignment1/summary.tex
+++ b/Assignment1/summary.tex
@@ -1,6 +1,7 @@
+\camil
 \subsection{Summary}
 % TODO: points to be added to 5.3
-\camil
+\emph{NB: these points are to be added to the current section 5.3.}
 \begin{itemize}
 	\item
 		PLTL is an extension to LTL which adds \emph{past modalities}.
diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex
index 81c1844..1090e5d 100644
--- a/Assignment1/syntax.tex
+++ b/Assignment1/syntax.tex
@@ -1,8 +1,8 @@
 \subsubsection{Syntax}
+\erin
 % 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