State of Büchi complementation
Journal
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Journal Volume
6482 LNCS
Pages
261-271
Date Issued
2011
Author(s)
Abstract
Büchi complementation has been studied for five decades since the formalism was introduced in 1960. Known complementation constructions can be classified into Ramsey-based, determinization-based, rank-based, and slice-based approaches. For the performance of these approaches, there have been several complexity analyses but very few experimental results. What especially lacks is a comparative experiment on all the four approaches to see how they perform in practice. In this paper, we review the state of Büchi complementation, propose several optimization heuristics, and perform comparative experimentation on the four approaches. The experimental results show that the determinization-based Safra-Piterman construction outperforms the other three and our heuristics substantially improve the Safra-Piterman construction and the slice-based construction. © 2011 Springer-Verlag Berlin Heidelberg.
Other Subjects
Comparative experiments; Complementation; Complementation constructions; Complexity analysis; Determinization; Optimization heuristics; Automata theory; Experiments
Type
conference paper