Lower Bounds on Witnesses for Nonemptiness of Universal co-Buchi Automata
=========================================================================
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
automata. 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 B\"uchi automata.
Alternating co-B\"uchi automata and witnesses to their nonemptiness
have applications in model checking (complementing a nondeterministic
B\"uchi word automaton results in a universal co-B\"uchi automaton)
and synthesis (an LTL specification can be translated to a universal
co-B\"uchi tree automaton accepting exactly all the transducers that
realize it). Emptiness algorithms for alternating co-B\"uchi automata
proceed by a translation to nondeterministic B\"uchi 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 automaton. It has
been conjectured that this super-exponential blow-up need not apply to
the length of the shortest witness. Intuitively, since co-B\"uchi
automata are memoryless, 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-B\"uchi 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-B\"uchi word and tree automata.