Kais Klai

In Proceedings of the 9th international symposium on automated technology for verification and analysis (ATVA’11)

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.

Combining explicit and symbolic approaches for better on-the-fly LTL model checking

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

2011-06-01

Abstract We present two new hybrid techniques that replace the synchronized product used in the automata-theoretic approach for LTL model checking. The proposed products are explicit graphs of aggregates (symbolic sets of states) that can be interpreted as Büchi automata. These hybrid approaches allow 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.

Self-loop aggregation product — a new hybrid approach to on-the-fly LTL model checking

Combining explicit and symbolic approaches for better on-the-fly LTL model checking

Search

Tags