Minimal Counterexample Generation for SPIN

We propose an algorithm to compute a counterexample of minimal size to some property in a finite state program, using the same space constraints than SPIN. This algorithm uses nested breadth-first searches guided by a priority queue. It works in time O(n2 log n) and is linear in memory.

• Type: Conference
• Year: 2007
• Where: SPIN
• Authors: Paul Gastin, Pierre Moro
• Keywords: Algorithm, Minimal Size, SPIN 2007, Theoretical Computer Science, finite State Program