Correct upper bound for bad prefixes

1 files changed, 31 insertions, 12 deletions

diff --git a/Assignment1/bad-prefix.tex b/Assignment1/bad-prefix.tex
index 0f80f79..a2101ba 100644
--- a/Assignment1/bad-prefix.tex
+++ b/Assignment1/bad-prefix.tex
@@ -1,5 +1,5 @@
 \camil
-\subsection{Minimal Bad Prefices}
+\subsection{Minimal Bad Prefixes}
 %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 4.4.3.}
 
@@ -23,8 +23,7 @@ Hence, $vw^j$ is a bad prefix.
 To find these $i,j$ for a given counterexample $vw^\omega$, one can simply \enquote{run} $TS \otimes \mathcal A$ with $vw^\omega$ and record the state of the automaton after every iteration of $w$.
 Once a state reoccurs, $j$ is found.
 This algorithm, more formally described in \cref{alg:bad-prefix}, is obviously guaranteed to find the smallest $i,j$ for which $vw^i$ and $vw^j$ lead to the same state.
-However, it is not guaranteed to find a minimal bad prefix.
-% TODO: counterexample
+However, it is not guaranteed to find a minimal bad prefix (for instance, when a prefix of $v$ already is a minimal bad prefix).
 
 \begin{algorithm}[H]
 	% NOTE: ugly hardcoded spacing to mimic ugly algorithm layout by Baier-Katoen
@@ -53,21 +52,41 @@ However, it is not guaranteed to find a minimal bad prefix.
 \end{algorithm}
 
 We can now prove an upper bound on the $j$ for which $vw^j$ is a bad prefix.
-This upper bound depends on the size of the NBA $\mathcal A$ that we construct for $\lnot P$.
-In general, $|\mathcal A| \le 2^{|P|}\cdot|P|$ as seen in Theorem 5.41.
-However, in the case of safety properties, the size of $\mathcal A$ can be shown to be smaller~\citep{Latvala2002,Latvala2003}:
-	$\mathcal A$ is bound by $2^{|\textit{tf}(P)|}$, where $\textit{tf}(\phi)$ are the temporal subformulas of $\phi$:
-This leads to an upper bound for the bad prefix returned by \cref{alg:bad-prefix}:
 
-\begin{theorem}[An Upper Bound for the Bad Prefix of a Counterexample]
-	If $vw^\omega$ is a counterexample for safety property $P$ in finite transition system $TS$, there exists a $j \le |TS|\cdot2^{|\textit{tf}(P)|}$ for which $vw^j$ is a bad prefix.
+\begin{theorem}[An Upper Bound for the Bad Prefix of Counterexamples]
+	\label{thm:bad-prefix:upper-bound}
+	If $vw^\omega$ is a counterexample for safety property $P$ in finite transition system $TS$, there exists a $j \le |TS|\cdot2^{|\lnot P|}\cdot|\lnot P|$ for which $vw^j$ is a bad prefix.
 
 	\begin{proof}
 		After $j$ iterations of the loop of \cref{alg:bad-prefix}, $S$ contains $j+1$ elements.
 		But since $S$ is a subset of the states of $TS \otimes\mathcal A$, it can contain at most $|TS \otimes\mathcal A|$ elements.
 		By the pigeonhole principle, a valid $j$ will be found in iteration $|TS\otimes\mathcal A|$ at the latest.
-		Combining this with the fact that $|\mathcal A| \le 2^{|\textit{tf}(P)|}$~\citep{Latvala2002,Latvala2003},
-			we know that $j \le |TS| \cdot 2^{|\textit{tf}(P)|}$.
+		Combining this with the fact that $|\mathcal A| \le 2^{|\lnot P|}\cdot|\lnot P|$ (see Theorem 5.41),
+			we know that $j \le |TS| \cdot 2^{|\lnot P|}\cdot|\lnot P|$.
 	\end{proof}
 \end{theorem}
+
+\begin{remark}[Finding Bad Prefixes of Counterexamples]
+	\Cref{alg:bad-prefix} would be rather inefficient in practice due to several factors:
+		the construction of NBA $\mathcal A$,
+		the synchronous product $TS \otimes \mathcal A$ and
+		the fact that we only check the state after full iterations of $w$.
+	Instead, we can also take a finite automaton $\mathcal A$ recognizing the \emph{informative prefixes} of $\lnot P$.%
+		\footnote{%
+			The \emph{informative prefixes} can informally be described as prefixes which \enquote{give all information} about why a property is not satisfied.
+			In most natural cases, the informative prefixes are exactly the bad prefixes.
+			A precise definition is given by \citet{Kupferman2001} but is not required here.}
+	This automaton $\mathcal A$ can be constructed with at most $2^{|\textit{rcl}(P)|}$ states~\citep{Latvala2003},%
+		\footnote{%
+			Here, $\textit{rcl}(\phi)$ is the restricted closure of $\phi$.
+			It contains all subformulas of $\phi$ with a temporal operator at their root, $\psi$ if it contains $\Xop\psi$, or $\phi$ itself if no other rule applies.}
+		for which an implementation exists.%
+			\footnote{\url{http://tcs.legacy.ics.tkk.fi/users/tlatvala/scheck/}}
+	To find a bad prefix, we now only need to run $\mathcal A$ with $vw^\omega$ until an accepting state is reached.
+
+	Since all bad prefixes are recognized by $\mathcal A$, this method in contrast to \cref{alg:bad-prefix} finds a minimal bad prefix.
+	However, it is not guaranteed to be of the form $vw^j$.
+	Combining the two results, the size of the minimal bad prefix in \enquote{natural} cases where all bad prefixes are informative is at most $|v|+|w|\cdot|TS|\cdot2^{|\lnot P|}\cdot|\lnot P|$.
+	In practice, the bad prefix will usually be much shorter.
+\end{remark}
 \cbend