Explicit State Model Checking with Generalized Büchi and Rabin Automata

Vincent Bloemen, Alexandre Duret-Lutz, Jaco van de Pol

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    1 Citation (Scopus)
    3 Downloads (Pure)


    In the automata theoretic approach to explicit state LTL model checking, the synchronized product of the model and an automaton that represents the negated formula is checked for emptiness. In practice, a (transition-based generalized) Büchi automaton (TGBA) is used for this procedure.
    This paper investigates whether using a more general form of acceptance, namely transition-based generalized Rabin automata (TGRAs), improves the model checking procedure. TGRAs can have signi cantly fewer states than TGBAs, however the corresponding emptiness checking procedure is more involved. With recent advances in probabilistic model checking and LTL to TGRA translators, it is only natural to ask whether checking a TGRA directly is more advantageous in practice.
    We designed a multi-core TGRA checking algorithm and performed experiments on a subset of the models and formulas from the 2015 Model Checking Contest. We observed that our algorithm can be used to replace a TGBA checking algorithm without losing performance. In general, we found little to no improvement by checking TGRAs directly.
    Original languageEnglish
    Title of host publicationSPIN 2017
    Subtitle of host publicationProceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software
    PublisherAssociation for Computing Machinery
    Number of pages10
    ISBN (Print)978-1-4503-5077-8
    Publication statusPublished - Jul 2017
    Event24th International SPIN Symposium 2017: Model Checking of Software - University of California, Santa Barbara, United States
    Duration: 13 Jul 201714 Jul 2017
    Conference number: 24


    Conference24th International SPIN Symposium 2017
    Abbreviated titleSPIN 2017
    Country/TerritoryUnited States
    CitySanta Barbara
    Internet address


    • Model checking
    • Explicit state
    • LTL
    • omega-automata
    • on-the-fly
    • generalised Büchi Automaton
    • generalised Rabin Automaton
    • parallel algorithms
    • multi-core


    Dive into the research topics of 'Explicit State Model Checking with Generalized Büchi and Rabin Automata'. Together they form a unique fingerprint.

    Cite this