diff options
Diffstat (limited to 'Assignment1/bad-prefix.tex')
| -rw-r--r-- | Assignment1/bad-prefix.tex | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/Assignment1/bad-prefix.tex b/Assignment1/bad-prefix.tex index 98e39ed..a1db684 100644 --- a/Assignment1/bad-prefix.tex +++ b/Assignment1/bad-prefix.tex @@ -1,2 +1,14 @@ -\subsubsection{Minimal Bad Prefix in NuSMV} +\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 |