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 automaton. 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-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. © 2011 Springer-Verlag.
CITATION STYLE
Duret-Lutz, A., Klai, K., Poitrenaud, D., & Thierry-Mieg, Y. (2011). Self-loop aggregation product - A new hybrid approach to on-the-fly LTL model checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6996 LNCS, pp. 336–350). https://doi.org/10.1007/978-3-642-24372-1_24
Mendeley helps you to discover research relevant for your work.