We show how to convert alternating Buchi 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 axe 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.
Symbolic Implementation of Alternating Automata / Bloem, R.; Cimatti, A.; Pill, I.; Roveri, M.; Semprini, S.. - 4094:(2006), pp. 208-218. ( 11th International Conference on Implementation and Application of Automata, CIAA 2006 Taipei, Taiwan 21/08/2006-23/08/2006) [10.1007/11812128_20].
Symbolic Implementation of Alternating Automata
A. Cimatti;M. Roveri;
2006-01-01
Abstract
We show how to convert alternating Buchi 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 axe 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
