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

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¨uchi 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¨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.

• Type: Journal
• Year: 2011
• Where: ATVA
• Authors: Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg
• Keywords: ATVA 2011, Hardware, Hybrid Technique, Space Thanks, Symbolic Approaches