Ramsey-Based Büchi Complementation
Stefan Breuers, Christof Löding, Jörg Olschewski · 2012
We consider complementing Buchi automata by applying the Ramsey-based approach, which is the original approach already used by Buchi and later improved by Sistla et al. We present several heuris- tics to reduce the state space of the resulting complement automaton and provide experimental data that shows that our improved construc- tion can compete (in terms of finished complementation tasks) also in practice with alternative constructions like rank-based complementation. Furthermore, we show how our techniques can be used to improve the Ramsey-based complementation such that the asymptotic upper bound for the resulting complement automaton is 2 O (n logn) instead of 2 O (n 2 ) .