Model checking with generalized Rabin and Fin-less automata

Authors

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

Journal

International Journal on Software Tools for Technology Transfer

Type

article

Publisher

Springer

Projects

Spot

Date

2019-04-01

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 TGBAshowever 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 directlywe 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.

Documents

• Paper

Bibtex (lrde.bib)

@Article{	  bloemen.19.sttt,
  author	= {Vincent Bloemen and Alexandre Duret-Lutz and Jaco van de
		  Pol},
  title		= {Model checking with generalized {R}abin and {F}in-less
		  automata},
  journal	= {International Journal on Software Tools for Technology
		  Transfer},
  publisher	= {Springer},
  month		= jun,
  volume	= 21,
  number	= 3,
  pages		= {307--324},
  year		= {2019},
  doi		= {10.1007/s10009-019-00508-4},
  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\"uchi 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.}
}