Ala Eddine Ben Salem

Combining explicit and symbolic LTL model checking using generalized testing automata

By Ala Eddine Ben Salem, Mohamed Graiet

2015-05-19

In Proceedings of the 15th international conference on application of concurrency to system design (ACSD’15)

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.

Continue reading

Extending testing automata to all LTL

By Ala Eddine Ben Salem

2015-05-19

In Proceedings of the 35th IFIP international conference on formal techniques for distributed objects, components and systems (FORTE’15)

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

Continue reading

Single-pass testing automata for LTL model checking

By Ala Eddine Ben Salem

2015-03-01

In Proceedings of the 9th international conference on language and automata theory and applications (LATA’15)

Abstract

Testing Automaton (TA) is a new kind of $\omega$-automaton introduced by Hansen et al. as an alternative to the standard Büchi Automata (BA) for the verification of stutter-invariant LTL properties. Geldenhuys and Hansen shown later how to use TA in the automata-theoretic approach to LTL model checking. They propose a TA-based approach using a verification algorithm that requires two searches (two passes) and compare its performance against the BA approach. This paper improves their work by proposing a transformation of TA into a normal form (STA) that only requires a single one-pass verification algorithm. The resulting automaton is called Single-pass Testing Automaton (STA). We have implemented the STA approach in Spot model checking library. We are thus able to compare it with the “traditional” BA and TA approaches. These experiments show that STA compete well on our examples.

Continue reading

Improving the model checking of stutter-invariant LTL properties

By Ala Eddine Ben Salem

2014-09-25

In

Abstract

Software systems have become ubiquitous in our everyday life. They replace humans for critical tasks that involve high costs and even human lives. The serious consequences caused by the failure of such systems make crucial the use of rigorous methods for system validation. One of the widely-used formal verification methods is the automata-theoretic approach to model checking. It takes as input a model of the system and a property, and answers if the model satisfies or not the property. To achieve this goal, it translates the negation of the property in an automaton and checks whether the product of the model and this automaton is empty. Although it is automatic, this approach suffers from the combinatorial explosion of the resulting product. To tackle this problem, especially when checking stutter-invariant LTL properties, we firstly improve the two-pass verification algorithm of Testing automata (TA), then we propose a transformation of TA into a normal form (STA) that only requires a single-pass verification algorithm. We also propose a new type of automata: the TGTA. These automata also enable a check in a single-pass and without adding artificial states : it combines the benefits of TA and generalized Büchi automata (TGBA). TGTA improve the explicit and symbolic model checking approaches. In particular, by combining TGTA with the saturation technique, the performances of the symbolic approach has been improved by an order of magnitude compared to TGBA. Used in hybrid approaches TGTA prove complementary to TGBA. All the contributions of this work have been implemented in SPOT and LTS-ITS, respectively, an explicit and a symbolic open source model-checking libraries.

Continue reading

Symbolic model checking of stutter invariant properties using generalized testing automata

By Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon, Yann Thierry-Mieg

2014-04-01

In Proceedings of the 20th international conference on tools and algorithms for the construction and analysis of systems (TACAS’14)

Abstract

In a previous work, we showed that a kind of $\omega$-automata known as Transition-based Generalized Testing Automata (TGTA) can outperform the Büchi automata traditionally used for explicit model checking when verifying stutter-invariant properties. In this work, we investigate the use of these generalized testing automata to improve symbolic model checking of stutter-invariant LTL properties. We propose an efficient symbolic encoding of stuttering transitions in the product between a model and a TGTA. Saturation techniques available for decision diagrams then benefit from the presence of stuttering self-loops on all states of TGTA. Experimentation of this approach confirms that it outperforms the symbolic approach based on (transition-based) Generalized Büchi Automata.

Continue reading

Model checking using generalized testing automata

By Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon

2012-03-01

In Transactions on Petri Nets and Other Models of Concurrency (ToPNoC VI)

Abstract

Geldenhuys and Hansen showed that a kind of $\omega$-automata known as Testing Automata (TA) can, in the case of stuttering-insensitive properties, outperform the Buchi automata traditionally used in the automata-theoretic approach to model checking. In previous work, we compared TA against Transition-based Generalized Buchi Automata (TGBA), and concluded that TA were more interesting when counterexamples were expected, otherwise TGBA were more efficient. In this work we introduce a new kind of automata, dubbed Transition-based Generalized Testing Automata (TGTA), that combine ideas from TA and TGBA. Implementation and experimentation of TGTA show that they outperform other approaches in most of the cases.

Continue reading

Generalized Büchi automata versus testing automata for model checking

By Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon

2011-05-25

In Proceedings of the second international workshop on scalable and usable model checking for petri net and other models of concurrency (SUMO’11)

Abstract

Geldenhuys and Hansen have shown that a kind of $\omega$-automaton known as testing automata can outperform the Buchi automata traditionally used in the automata-theoretic approach to model checking (geldenhuys.06.spin?). This work completes their experiments by including a comparison with generalized Buchi automata; by using larger state spaces derived from Petri nets; and by distinguishing violated formulæ (for which testing automata fare better) from verified formulæ (where testing automata are hindered by their two-pass emptiness check).

Continue reading

Search

Tags