Symbolic Implementation of Alternating Automata

This paper addresses the challenges of symbolic model checking and language emptiness checking where the specification is given as an alternating Buchi automaton.We introduce a novel version of Miyano and Hayashi's construction that allows us to directly convert an alternating automaton to a polynomially-sized symbolic structure. We thus avoid building an exponentially-sized explicit representation of the corresponding nondeterministic automaton.For one-weak automata, Gastin and Oddoux' construction produces smaller automata than Miyano and Hayashi's construction. We present a (symbolic) hybrid approach that combines the benefits of both: while retaining full generality, it uses the cheaper construction for those parts of the automaton that are one-weak.We performed a thorough experimental comparison of the explicit and symbolic approaches and several variants of Miyano and Hayashi's construction, using both BDD-based and SAT-based model checking techniques. The symbolic approaches cle...