\camil
\subsection{Minimal Bad Prefixes}
\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.

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 (for instance, when a prefix of $v$ already is a minimal bad prefix).

% TODO: fix placement; see https://tex.stackexchange.com/q/427278/23992
\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.

	\vspace{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.

\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^{|\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