From complementation to certification

In this paper we analyze runs of NGBW and use the analysis in order to describe a new complementation construction and a symbolic emptiness algorithm for NGBW. The complementation construction exponentially improves the best known construction for NGBW and is easy to implement. The emptiness algorithm is almost identical to a known variant of the Emerson-Lei algorithm, and our contribution is the strong relation we draw between the complementation construction and the emptiness algorithm-both naturally follow from the analysis of the runs, which easily implies their correctness. This relation leads to a new certified model-checking procedure, where a positive answer to the model-checking query is accompanied by a certificate whose correctness can be checked by methods independent of the model checker. Unlike certificates generated in previous works on certified model checking, our analysis enables us to generate a certificate that can be checked automatically and symbolically.