I am happy to announce that the following paper has been accepted in
the Conference on Formal Techniques for Distributed Objects,
Components and Systems (FORTE'15), to be held in Grenoble on June 2-5, 2015.
Extending Testing Automata to All LTL
Ala Eddine Ben Salem
LRDE, EPITA, Le Kremlin-Bicêtre, France, ala(a)lrde.epita.fr
Abstract:
An alternative to the traditional Büchi Automata (BA), called Testing
Automata (TA) was proposed by Hansen et al. to improve the automata
theoretic approach to LTL model checking. In previous work, we proposed
an improvement of this alternative approach called TGTA (Generalized Testing
Automata). TGTA mixes features from both TA and TGBA (Generalized Büchi
Automata), without the disadvantage of TA, which is the second pass of the
emptiness check algorithm. We have shown that TGTA outperform TA, BA and
TGBA for explicit and symbolic LTL model checking. However, TA and TGTA
are less expressive than Büchi Automata since they are able to represent only
stutter-invariant LTL properties (LTL\X). In this paper, we show how to
extend Generalized Testing Automata (TGTA) to represent any LTL property.
This allows to extend the model checking approach based on this new form of
testing automata to check other kinds of properties and also other kinds of models
(such as Timed models). Implementation and experimentation of this extended
TGTA approach show that it is statistically more efficient than the Büchi Automata
approaches (BA and TGBA), for the explicit model checking of LTL properties.
Show replies by date
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.