The automata-theoretic approach to model checking reduces a model checking problem to automata constructions and automata decision problems. In particular, a linear time specification is translated into an equivalent automata, then complemented, composed with the transition system, and finally checked for emptiness.

In this talk I will present new results related to the complementation of alternating automata with the parity acceptance condition (APW), how to translate temporal logic specifications into APW with few colors, and efficient translations from APW into nondeterministic Buchi automata (NBW) that can be the basis for emptiness checking.