Co-Büching them all

Abstract. We solve the open problems of translating, when possible, all common classes of nondeterministic word automata to deterministic and nondeterminis-tic co-Büchi word automata. The handled classes include Büchi, parity, Rabin, Streett and Muller automata. The translations follow a unified approach and are all asymptotically tight. The problem of translating Büchi automata to equivalent co-Büchi automata was solved in [2], leaving open the problems of translating automata with richer ac-ceptance conditions. For these classes, one cannot easily extend or use the con-struction in [2]. In particular, going via an intermediate Büchi automaton is not optimal and might involve a blow-up exponentially higher than the known lower bound. Other known translations are also not optimal and involve a doubly expo-nential blow-up. We describe direct, simple, and asymptotically tight constructions, involving a 2 Θ(n) blow-up. The constructions are variants of the subset construction, and allow for symbolic implementations. Beyond the theoretical importance of the results, the new constructions have various applications, among which is an im-proved algorithm for translating, when possible, LTL formulas to deterministic Büchi word automata.