Efficient model checking via büchi tableau automata

Girish S. Bhat, Rance Cleaveland, Alex Groce

Research output: Chapter in Book/Report/Conference proceedingConference contribution

19 Scopus citations


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 methodology is based on the "compilation" of temporal formulas into variants of alternating tree automata called alternating BUchi 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 model checkers targeted 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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 13th International Conference, CAV 2001, Proceedings
EditorsHubert Comon, Alain Finkel, Gérard Berry
Number of pages15
ISBN (Print)3540423451
StatePublished - 2001
Externally publishedYes
Event13th International Conference on Computer Aided Verification, CAV 2001 - Paris, France
Duration: Jul 18 2001Jul 22 2001

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference13th International Conference on Computer Aided Verification, CAV 2001

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Efficient model checking via büchi tableau automata'. Together they form a unique fingerprint.

Cite this