1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
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 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.
% 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
|
