Publication: Extending Testing Automata to All LTL (FORTE'15)

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@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.

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@lrde.epita.fr (2) Institut Supérieur d’Informatique et de Mathématiques de Monastir, Tunisie, Mohamed.Graiet@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.
participants (2)
-
Ala Eddine BEN SALEM
-
Daniela Becker