Model checking with generalized Rabin and Fin-less automata

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

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

3 Citations (Scopus)
37 Downloads (Pure)

Abstract

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 a transition-based generalized Rabin automaton (TGRA), improves the model checking procedure. TGRAs can have significantly 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 and generated LTL formulas for models from the BEEM database. While we found little to no improvement by checking TGRAs directly, we show how various aspects of a TGRA’s structure influences the model checking performance. In this paper, we also introduce a Fin-less acceptance condition, which is a disjunction of TGBAs. We show how to convert TGRAs into automata with Fin-less acceptance and show how a TGBA emptiness procedure can be extended to check Fin-less automata.

Original languageEnglish
Pages (from-to)307-324
Number of pages18
JournalInternational journal on software tools for technology transfer
Volume21
Issue number3
DOIs
Publication statusPublished - 1 Jun 2019

Keywords

  • Büchi
  • Explicit state
  • Generalized
  • LTL
  • Model checking
  • Multi-core
  • On-the-fly
  • Parallel
  • Rabin
  • ω-Automata

Fingerprint

Dive into the research topics of 'Model checking with generalized Rabin and Fin-less automata'. Together they form a unique fingerprint.

Cite this