## Efficient Model Checking Via Buechi Tableau Automata

### Girish Bhat, Rance Cleaveland, Alex Groce

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001

## Abstract

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.

 Server START Conference Manager Update Time 28 Mar 2001 at 08:36:01 Maintainer www-cav01@lsv.ens-cachan.fr.
 Conference Systems