This paper addresses the challenges of symbolic model checking and language emptiness checking where the specification is given as an alternating Büchi 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 clearly outperform the explicit one.
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach
