Improved Ramsey-based Büchi Complementation

Foundations of Software Science and Computational Structures (FoSSaCS'12)

We consider complementing Büchi automata by applying the Ramsey-based approach, which is the original approach already used by Büchi and later improved by Sistla et al. We present several heuristics to reduce the state space of the resulting complement automaton and provide experimental data that shows that our improved construction 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 log n) instead of 2^O(n2).

@incollection{breuers2012improved,
title={Improved Ramsey-based B{\"u}chi Complementation},
author={Breuers, Stefan and L{\"o}ding, Christof and Olschewski, J{\"o}rg},
booktitle={Foundations of Software Science and Computational Structures},
pages={150--164},
year={2012},
publisher={Springer}
}

Downloads:
Paper