From Complementation to Certification
=====================================
In the automata-theoretic approach to model checking we check the
emptiness of the product of a system $S$ with an automaton $\A_{\neg
\psi}$ for the complemented specification. This gives rise to two
automata-theoretic problems: {\em complementation\/} of word automata,
which is used in order to generate $\A_{\neg \psi}$, and the {\em
emptiness\/} problem, to which model checking is reduced. Both
problems have numerous other applications, and have been extensively
studied for nondeterministic B\"uchi word automata (NBW).
Nondeterministic {\em generalized\/} B\"uchi word automata (NGBW) have
become popular in specification and verification and are now used in
applications traditionally assigned to NBW. This is due to their
richer acceptance condition, which leads to automata with fewer states
and a simpler underlying structure.
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 {\em 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.