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.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte di FBK.
Titolo: | Symbolic Implementation of Alternating Automata |
Autori: | |
Data di pubblicazione: | 2007 |
Rivista: | |
Abstract: | 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. |
Handle: | http://hdl.handle.net/11582/4321 |
Appare nelle tipologie: | 1.1 Articolo in rivista |