Minimization of Counterexamples in SPIN

We propose an algorithm to find a counterexample to some property in a finite state program. This algorithm is derived from SPIN’s one, but it finds a counterexample faster than SPIN does. In particular it still works in linear time. Compared with SPIN’s algorithm, it requires only one additional bit per state stored. We further propose another algorithm to compute a counterexample of minimal size. Again, this algorithm does not use more memory than SPIN does to approximate a minimal counterexample. The cost to find a counterexample of minimal size is that one has to revisit more states than SPIN. We provide an implementation and discuss experimental results.

• Type: Conference
• Year: 2004
• Where: SPIN
• Authors: Paul Gastin, Pierre Moro, Marc Zeitoun
• Keywords: Algorithm, Counterexample, Minimal Size, SPIN 2004, Theoretical Computer Science