Self-Loop Aggregation Product — A New Hybrid Approach to On-the-Fly LTL Model Checking

Authors

Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg

Where

Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11)

Place

Taipei, Taiwan

Type

inproceedings

Publisher

Springer

Projects

Spot

Date

2011-06-23

Abstract

We present the Self-Loop Aggregation Product (SLAP), a new hybrid technique that replaces the synchronized product used in the automata-theoretic approach for LTL model checking. The proposed product is an explicit graph of aggregates (symbolic sets of states) that can be interpreted as a Büchi automata. The criterion used by SLAP to aggregate states from the Kripke structure is based on the analysis of self-loops that occur in the Büchi automaton expressing the property to verify. Our hybrid approach allows on the one hand to use classical emptiness-check algorithms and build the graph on-the-flyand on the other hand, to have a compact encoding of the state space thanks to the symbolic representation of the aggregates. Our experiments show that this technique often outperforms other existing (hybrid or fully symbolic) approaches.

Documents

• Paper

• Slides

Bibtex (lrde.bib)

@InProceedings{	  duret.11.atva,
  author	= {Alexandre Duret-Lutz and Kais Klai and Denis Poitrenaud
		  and Yann Thierry-Mieg},
  title		= {Self-Loop Aggregation Product --- A New Hybrid Approach to
		  On-the-Fly {LTL} Model Checking},
  booktitle	= {Proceedings of the 9th International Symposium on
		  Automated Technology for Verification and Analysis
		  (ATVA'11)},
  year		= 2011,
  series	= {Lecture Notes in Computer Science},
  volume	= 6996,
  pages		= {336--350},
  address	= {Taipei, Taiwan},
  month		= oct,
  publisher	= {Springer},
  abstract	= {We present the \emph{Self-Loop Aggregation Product}
		  (SLAP), a new hybrid technique that replaces the
		  synchronized product used in the automata-theoretic
		  approach for LTL model checking. The proposed product is an
		  explicit graph of aggregates (symbolic sets of states) that
		  can be interpreted as a B\"uchi automata. The criterion
		  used by SLAP to aggregate states from the Kripke structure
		  is based on the analysis of self-loops that occur in the
		  B\"uchi automaton expressing the property to verify. Our
		  hybrid approach allows on the one hand to use classical
		  emptiness-check algorithms and build the graph on-the-fly,
		  and on the other hand, to have a compact encoding of the
		  state space thanks to the symbolic representation of the
		  aggregates. Our experiments show that this technique often
		  outperforms other existing (hybrid or fully symbolic)
		  approaches.},
  doi		= {10.1007/978-3-642-24372-1_24}
}