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


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.
Start Conference Manager
Conference Systems