This paper describes an approach to engineering efficient model checkers that
are generic with respect to the temporal logic in which system properties are
given. The approach is based on the ``compilation'' of temporal formulas into
variants of alternating tree automata called \emph{alternating B\"uchi tableau
automata} (ABTAs). The paper gives an efficient on-the-fly model-checking
procedure for ABTAs and illustrates how translations of temporal logics into
ABTAs may be concisely specified using inference rules, which may be thus seen
as high-level definitions of ``model checkers'' for the logic given.
Heuristics for simplifying ABTAs are also given, as are experimental results
in the CWB-NC verification tool suggesting that, despite the generic ABTA
basis, our approach can perform better than hand-coded model checkers for
specific logics. The ABTA-based approach we advocate simplifies the
retargeting of model checkers to different logics, and it also allows the use
of ``compile-time'' simplifications on ABTAs that improves model-checker
performance.
