Buchi Complementation Made Tighter
==================================
The complementation problem for nondeterministic word automata has
numerous applications in formal verification. In particular, the
language-containment problem, to which many verification problems is
reduced, involves complementation. For automata on finite words,
which correspond to safety properties, complementation involves
determinization. The 2^n blow-up that is caused by the subset
construction is justified by a tight lower bound. For B\"uchi
automata on infinite words, which are required for the modeling of
liveness properties, optimal complementation constructions are quite
complicated, as the subset construction is not sufficient. From a
theoretical point of view, the problem is considered solved since
1988, when Safra came up with a determinization construction for
B\"uchi automata, leading to a 2^{O(n log n)} complementation
construction, and Michel came up with a matching lower bound. A
careful analysis, however, of the exact blow-up in Safra's and
Michel's bounds reveals an exponential gap in the constants hiding in
the O() notations: while the upper bound on the number of states in
Safra's complementary automaton is n^{2n}, Michel's lower bound
involves only an n! blow up, which is roughly (n/e)^n. The
exponential gap exists also in more recent complementation
constructions. In particular, the upper bound on the number of states
in the complementation construction in [KV01], which avoids
determinization, is (6n)^n. This is in contrast with the case of
automata on finite words, where the upper and lower bounds
coincides. In this work we describe an improved complementation
construction for nondeterministic B\"uchi automata and analyze its
complexity. We show that the new construction results in an automaton
with at most (1.06n)^n states. While this leaves the problem about
the exact blow up open, the gap is now exponentially smaller. From a
practical point of view, our solution enjoys the simplicity of [KV01],
and results in much smaller automata.