Combining Explicit and Symbolic LTL Model Checking Using Generalized Testing Automata

Authors

Ala Eddine Ben Salem, Mohamed Graiet

Where

Proceedings of the 15th International Conference on Application of Concurrency to System Design (ACSD'15)

Place

Brussels, Belgium

Type

inproceedings

Publisher

IEEE Computer Society

Projects

Spot

Date

2015-05-19

Abstract

In automata-theoretic model checking, there are mainly two approaches: explicit and emphsymbolic. In the explicit approach, the state-space is constructed explicitly and lazily during exploration (i.e.on-the-fly). The symbolic approach tries to overcome the state-space explosion obstacle by symbolically encoding the state-space in a concise way using decision diagrams. However, this symbolic construction is not performed on-the-fly as in the explicit approach. In order to take advantage of the best of both worlds, emphhybrid approaches are proposed as combinations of explicit and symbolic approaches. A hybrid approach is usually based on an on-the-fly construction of an explicit graph of symbolic nodes, where each symbolic node encodes a subset of states by means of binary decision diagrams. An alternative to the standard Büchi automata, called Testing automata have never been used before for hybrid model checking. In addition, in previous work, we have shown that Generalized Testing Automata (TGTA) can outperform the Büchi automata for explicit and symbolic model checking of stutter-invariant LTL properties. In this workwe investigate the use of these TGTA to improve hybrid model checking. We show how traditional hybrid approaches based on Generalized Büchi Automata (TGBA) can be adapted to obtain TGTA-based hybrid approaches. Then, each original approach is experimentally compared against its TGTA variant. The results show that these new variants are statistically more efficient.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  bensalem.15.acsd,
  author	= {Ala Eddine Ben{ S}alem and Mohamed Graiet},
  title		= {Combining Explicit and Symbolic {LTL} Model Checking Using
		  Generalized Testing Automata},
  booktitle	= {Proceedings of the 15th International Conference on
		  Application of Concurrency to System Design (ACSD'15)},
  year		= 2015,
  address	= {Brussels, Belgium},
  month		= jun,
  publisher	= {IEEE Computer Society},
  abstract	= {In automata-theoretic model checking, there are mainly two
		  approaches: \emph{explicit} and \emph{symbolic}. In the
		  explicit approach, the state-space is constructed
		  explicitly and lazily during exploration (i.e.,
		  on-the-fly). The symbolic approach tries to overcome the
		  state-space explosion obstacle by symbolically encoding the
		  state-space in a concise way using decision diagrams.
		  However, this symbolic construction is not performed
		  on-the-fly as in the explicit approach. In order to take
		  advantage of the best of both worlds, \emph{hybrid
		  approaches} are proposed as combinations of explicit and
		  symbolic approaches. A hybrid approach is usually based on
		  an on-the-fly construction of an explicit graph of symbolic
		  nodes, where each symbolic node encodes a subset of states
		  by means of binary decision diagrams. An alternative to the
		  standard {B\"u}chi automata, called Testing automata have
		  never been used before for hybrid model checking. In
		  addition, in previous work, we have shown that
		  \emph{Generalized Testing Automata} (TGTA) can outperform
		  the {B\"u}chi automata for explicit and symbolic model
		  checking of stutter-invariant LTL properties. In this work,
		  we investigate the use of these TGTA to improve hybrid
		  model checking. We show how traditional hybrid approaches
		  based on Generalized {B\"u}chi Automata (TGBA) can be
		  adapted to obtain TGTA-based hybrid approaches. Then, each
		  original approach is experimentally compared against its
		  TGTA variant. The results show that these new variants are
		  statistically more efficient. }
}