On the complexity of parity word automata

Abstract

Different types of nondeterministic automata on infinite words differ in their succinctness and in the complexity for their nonemptiness problem. A simple translation of a parity automaton to an equivalent Büchi automaton is quadratic: a parity automaton with n states, m transitions, and index k may result in a Büchi automaton of size O((n + m)k). The best known algorithm for the nonemptiness problem of parity automata goes through Büchi automata, leading to a complexity of O((n +m)k). In this paper we show that while the translation of parity automata to Büchi automata cannot be improved, the special structure of the acceptance condition of parity automata can be used in order to solve the nonemptiness problem directly, with a dynamic graph algorithm of complexity O((n + m) log k).