I am happy to announce that the following paper has been accepted in
the 15th International Conference on Application of Concurrency to
System Design (ACSD'15), to be held in Brussels on June 21-26, 2015.
Combining Explicit and Symbolic LTL Model Checking
Using Generalized Testing Automata
Ala Eddine Ben Salem (1) and Mohamed Graiet (2)
(1) LRDE, EPITA, Le Kremlin-Bicêtre, France, ala(a)lrde.epita.fr
(2) Institut Supérieur d’Informatique et de Mathématiques
de Monastir, Tunisie, Mohamed.Graiet(a)imag.fr
Abstract:
In automata-theoretic model checking, there are mainly two approaches:
explicit and symbolic.
In the explicit approach, the state-space is constructed explicitly and
lazily during exploration (i.e., on-the-fly).
The symbolic approach tries to overcome the state-space explosion
obstacle by symbolically encoding the state-space in a concise way using
decision diagrams. However, this symbolic construction is not performed
on-the-fly as in the explicit approach.
In order to take advantage of the best of both worlds, hybrid approaches
are proposed as combinations of explicit and symbolic approaches.
A hybrid approach is usually based on an on-the-fly construction of an
explicit graph of symbolic nodes, where each symbolic node encodes a
subset of states by means of binary decision diagrams.
An alternative to the standard Büchi automata, called Testing automata
have never been used before for hybrid model checking. In addition, in
previous work, we have shown that Generalized Testing Automata (TGTA)
can outperform the Büchi automata for explicit and symbolic model
checking of stutter-invariant LTL properties.
In this work, we investigate the use of these TGTA to improve hybrid
model checking. We show how traditional hybrid approaches based on
Generalized Büchi Automata (TGBA) can be adapted to obtain TGTA-based
hybrid approaches. Then, each original approach is experimentally
compared against its TGTA variant. The results show that these new
variants are statistically more efficient.