This article presents a new algorithm for finding a minimal counterexample in explicit state model checking with B?uchi automata. The algorithm is an interleaved breadthfirst 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 B?uchi 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.