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

## 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.

## 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},
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}
}