Symbolic Implementation of Alternating Automata

We show how to convert alternating B¨uchi automata to symbolic structures, using a variant of Miyano and Hayashi’s construction. We avoid building the nondeterministic equivalent of the alternating automaton, thus save an exponential factor in space. For one-weak automata, Miyano and Hayashi’s approach produces automata that are larger than needed. We show a hybrid approach that produces a smaller nondeterministic automaton if part of the alternating automaton is one weak. We perform a thorough experimental analysis and conclude that the symbolic approach outperforms the explicit one.