A polynomial-time algorithm for the automatic Baire property
Ludwig Staiger
TL;DR
The paper develops a polynomial-time framework for the automatic Baire property in the Cantor space by starting from a Muller automaton for a regular ω-language and constructing Muller and Büchi automata that define the corresponding open and meagre components. It leverages a detailed analysis of loop structures, SCCs, and density to obtain a decomposition into open and meagre parts and to ensure that the resulting automata have manageable sizes. A key contribution is a polynomial-time Muller-to-Büchi translation under a maximal-loops condition, enabling efficient automata-based representations of the automatic Baire property. The results facilitate practical verification and analysis of topological regular ω-languages using standard graph algorithms, with implications for automated reasoning over infinite words and descriptive set-theoretic properties.
Abstract
A subset of a topological space possesses the Baire property if it can be covered by an open set up to a meagre set. For the Cantor space of infinite words Finkel introduced the automatic Baire category where both sets, the open and the meagre, can be chosen to be definable by finite automata. Here we show that, given a Muller automaton defining the original set, resulting open and meagre sets can be constructed in polynomial time. Since the constructed sets are of simple topological structure, it is possible to construct not only Muller automata defining them but also the simpler Büchi automata. To this end we give, for a restricted class of Muller automata, a conversion to equivalent Büchi automata of at most quadratic size.