More Deterministic" vs. "Smaller" Buechi Automata for Efficient LTL Model Checking"

The standard technique for LTL model checking ($M\models\neg\vi$) consists on translating the negation of the LTL specification, $\vi$, into a Buechi automaton $A_\vi$, and then on checking if the product $M \times A_\vi$ has an empty language. The efforts to maximize the efficiency of this process have so far concentrated on developing translation algorithms producing Buechi automata which are as small as possible, under the implicit conjecture that this fact should make the final product smaller. In this paper we build on a different conjecture and present an alternative approach in which we generate instead Buechi automata which are as deterministic as possible, in the sense that we try to reduce as much as we are able to the presence of non-deterministic decision states in $A_\vi$. We motivate our choice and present some empirical tests to support this approach.