Tight bounds for the determinisation and complementation of generalised Büchi automata

Abstract

Generalised Büchi automata are Büchi automata with multiple accepting sets. They form a class of automata that naturally occurs, e.g., in the translation from LTL to ω-automata. In this paper, we extend current determinisation techniques for Büchi automata to generalised Büchi automata and prove that our determinisation is optimal. We show how our optimal determinisation technique can be used as a foundation for complementation and establish that the resulting complementation is tight. Moreover, we show how this connects the optimal determinisation and complementation techniques for ordinary Büchi automata. © 2012 Springer-Verlag.