Minimal separating sets for acceptance conditions in Muller Automata

For a Muller automaton only a subset of its states is needed to decide whether a run is accepting or not. The set I of the infinitely often visited states can be replaced by the intersection I∩W with a fixed set W of states, provided W is large enough to distinguish between accepting and non-accepting loops in the automaton. We call such a subset W a separating set. Whereas the idea was previously introduced by McNaughton (Ann. Pure Appl. Logic 65 (1993) 149–184), the algorithmic construction of the smallest separating sets is not treated in the literature. In this paper we show that the problem whether in a Muller automaton a separating set of a given size exists is NP-complete. As a step towards an efficient computation of a separating set of minimal size we present an algorithm in the second part of the paper, based on an analysis of the loop structure of the given automaton.