Upper bound for minimal bad prefices

1 files changed, 64 insertions, 5 deletions

diff --git a/Assignment1/bad-prefix.tex b/Assignment1/bad-prefix.tex
index a1db684..0f80f79 100644
--- a/Assignment1/bad-prefix.tex
+++ b/Assignment1/bad-prefix.tex
@@ -1,14 +1,73 @@
 \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.}
+\emph{NB: this section is not particularly about PLTL. It is better added as 4.4.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 a finite transition system $TS$ violates safety property $P$ with the counterexample $vw^\omega$.
+There is a straightforward way to extract a bad prefix from $vw^\omega$, which is outlined below.
 
-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.
+Recall from section 5.2 that to verify a property $\phi$ we construct an NBA $\mathcal A$ with $\mathcal L_\omega(\mathcal A) = \textsl{Words}(\lnot\phi)$.
+Then, we check whether there exists a path in $TS \otimes \mathcal A$ satisfying the acceptance criterion of $\mathcal A$.
+A counterexample $vw^\omega$ is a path in $TS \otimes \mathcal A$.
+Since $P$ is a safety property and $w$ is repeated infinitely often, there exists an $i$ such that $vw^i \in \textsl{BadPref}(P)$.
+
+If we now have $0 \le i < j$ and a state $q$ such that $TS \otimes \mathcal A \xrightarrow{vw^i} q$ and $TS \otimes \mathcal A \xrightarrow{vw^j} q$, then $vw^j$ is a bad prefix.
+If not, there would be a $k$ with $vw^jw^ku \vDash P$.
+But then we have $\sigma \vDash P$ for all $\sigma = vw^jw^{(j-i)^n}w^ku$ ($n\in\mathbb N$), since $q \xrightarrow{w^{j-i}} q$.
+Then no bad prefix would exist, while we know that all counterexamples to safety properties contain a bad prefix.
+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
+
+\begin{algorithm}[H]
+	% NOTE: ugly hardcoded spacing to mimic ugly algorithm layout by Baier-Katoen
+	\caption{Finding a bad prefix for a safety property from a counterexample $vw^\omega$}
+	\label{alg:bad-prefix}
+	\vspace{5pt}
+	\textit{Input:} finite transition system $TS$, safety property $P$ and a counterexample $vw^\omega$.\\
+	\textit{Output:} an $i\in\mathbb N$ for which $vw^i$ is a bad prefix.\\[-5pt]
+	\hrule
+	\begin{algorithmic}[0]
+		\State $\mathcal A \gets \text{an NBA such that $\mathcal L_\omega(\mathcal A) = \textsl{Words}(\lnot P)$}$
+		\State $M \gets TS \otimes \mathcal A$
+		\State $q \gets \delta^*(M, v)$
+		\State $S \gets \{q\}$
+		\State $i \gets 0$
+		\Loop
+			\State $i \gets i + 1$
+			\State $q \gets \delta^*(q, w)$
+			\If{$q \in S$}
+				\State \Return $i$
+			\Else
+				\State $S \gets S \cup \{q\}$
+			\EndIf
+		\EndLoop
+	\end{algorithmic}
+\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{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)|}$.
+	\end{proof}
+\end{theorem}
 \cbend