Minimizing Generalized Buchi Automata

We consider the problem of minimization of generalized Buchi automata. We show how to extend fair simulation and delayed simulation to the case where the Buchi automaton has multiple acceptance conditions. For fair simulation, we show how to efficiently compute the fair-simulation relation while maintaining the structure of the automaton. We then use the fair-simulation relation to merge states and remove transitions. Our fair-simulation algorithm works in time $O(mn^2k^2)$ where $m$ is the number of transitions, $n$ is the number of states, and $k$ is the number of acceptance sets. For delayed simulation, we extend the existing definition to the case of multiple acceptance condition. We show that our definition can indeed be used for minimization and give an algorithm that computes the delayed-simulation relation. Our delayed-simulation algorithm works in time $O(mn^2k)$. We implemented the two algorithms and report on experimental results.