The Büchi complementation saga

Abstract. The complementation problem for nondeterministic word au-tomata has numerous applications in formal verification. In particular, the language-containment problem, to which many verification problems are reduced, involves complementation. For automata on finite words, which correspond to safety properties, complementation involves deter-minization. The 2n blow-up that is caused by the subset construction is justified by a tight lower bound. For Büchi automata on infinite words, which are required for the modeling of liveness properties, optimal com-plementation constructions are quite complicated, as the subset construc-tion is not sufficient. We review here progress on this problem, which dates back to its introduction in Büchi’s seminal 1962 paper.