Lower Bounds on Witnesses for Nonemptiness of
Universal Co-B, Orna Kupferman, Nir Piterman · 2009
The nonemptiness problem for nondeterministic automata on infinite words can be reduced to a sequence of reachability queries. The length of a shortest witness to the nonemptiness is then polynomial in the automaton. Nonemptiness algorithms for alternating automata translate them to nondeterministic automata. The exponential blow-up that the translation involves is justified by lower bounds for the nonemptiness problem, which is exponentially harder for alternating au- tomata. The translation to nondeterministic automata also entails a blow-up in the length of the shortest witness. A matching lower bound here is known for cases where the translation involves a 2 O(n) blow up, as is the case for finite words or Buchi automata. Alternating co-Buchi automata and witnesses to their nonemptiness have appli- cations in model checking (complementing a nondeterministic Buchi word automa- ton results in a universal co-Buchi automaton) and synthesis (an LTL specification can be translated to a universal co-Buchi tree automaton accepting exactly all the transducers that realize it). Emptiness algorithms for alternating co-Buchi automata proceed by a translation to nondeterministic Buchi automata. The blow up here is 2 O(n log n) , and it follows from the fact that, on top of the subset construction, the nondeterministic automaton maintains ranks to the states of the alternating automa- ton. It has been conjectured that this super-exponential blow-up need not apply to the length of the shortest witness. Intuitively, since co-Buchi automata are memo- ryless, it looks like a shortest witness need not visit a state associated with the same set of states more than once. A similar conjecture has been made for the width of a transducer generating a tree accepted by an alternating co-Buchi tree automaton. We show that, unfortunately, this is not the case, and that the super-exponential lower bound on the witness applies already for universal co-Buchi word and tree automata.