Minimal Counterexamples in O(n log n) Memory and O(n^2) Time

This article presents a new algorithm for finding a minimal counterexample in explicit state model checking with Buchi automata. The algorithm is an interleaved breadth-first search that explores some transitions backwards. We prove the correctness of our algorithm, along with complexity results. The worst-case time consumption of a simple version of our algorithm is proportional to the number of states and transitions, times the number of Buchi states. We also derive some simple yet efficient ways of reducing the search using the mathematical properties of minimal counterexamples. The properties are very general, and should be applicable to other approaches as well