blob: a1db68405e162bd7389fb46aa6fe81b6dd8df6cc (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
\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
|
