Fabrice Kordon

Strength-based decomposition of the property Büchi automaton for faster model checking

By Étienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud

2013-01-08

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

Abstract

The automata-theoretic approach for model checking of linear-time temporal properties involves the emptiness check of a large Büchi automaton. Specialized emptiness-check algorithms have been proposed for the cases where the property is represented by a weak or terminal automaton. When the property automaton does not fall into these categories, a general emptiness check is required. This paper focuses on this class of properties. We refine previous approaches by classifying strongly-connected components rather than automata, and suggest a decomposition of the property automaton into three smaller automata capturing the terminal, weak, and the remaining strong behaviors of the property. The three corresponding emptiness checks can be performed independently, using the most appropriate algorithm. Such a decomposition approach can be used with any automata-based model checker. We illustrate the interest of this new approach using explicit and symbolic LTL model checkers.

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

polyDD: Towards a framework generalizing decision diagrams

By Alban Linard, Emmanuel Paviot-Adet, Fabrice Kordon, Didier Buchs, Samuel Charron

2010-06-01

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

Abstract

Decision Diagrams are now widely used in model checking as extremely compact representations of state spaces. Many Decision Diagram categories have been developed over the past twenty years based on the same principles. Each one targets a specific domain with its own characteristics. Moreover, each one provides its own definition. It prevents sharing concepts and techniques between these structures. This paper aims to propose a basis for a common Framework for Decision Diagrams. It should help users of this technology to define new Decision Diagram categories thanks to a simple specification mechanism called Controller. This enables the building of efficient Decision Diagrams dedicated to a given problem.

Continue reading

Building efficient model checkers using hierarchical set decision diagrams and automatic saturation

By Alexandre Hamez, Yann Thierry-Mieg, Fabrice Kordon

2009-08-01

In Fundamenta Informaticae

Abstract

Shared decision diagram representations of a state-space provide efficient solutions for model-checking of large systems. However, decision diagram manipulation is tricky, as the construction procedure is liable to produce intractable intermediate structures (a.k.a peak effect). The definition of the so-called saturation method has empirically been shown to mostly avoid this peak effect, and allows verification of much larger systems. However, applying this algorithm currently requires deep knowledge of the decision diagram data-structures. Hierarchical Set Decision Diagrams (SDD) are decision diagrams in which arcs of the structure are labeled with sets, themselves stored as SDD. This data structure offers an elegant and very efficient way of encoding structured specifications using decision diagram technology. It also offers, through the concept of inductive homomorphisms, flexibility to a user defining a transition relation. We show in this paper how, with very limited user input, the SDD library is able to optimize evaluation of a transition relation to produce a saturation effect at runtime. We build as an example an SDD model-checker for a compositional formalism: Instantiable Petri Nets (IPN). IPN define a type as an abstract contract. Labeled P/T nets are used as an elementary type. A composite type is defined to hierarchically contain instances (of elementary or composite type). To compose behaviors, IPN use classic label synchronization semantics from process calculi. With a particular recursive folding SDD are able to offer solutions for symmetric systems in logarithmic complexity with respect to other DD. Even in less regular cases, the use of hierarchy in the specification is shown to be well supported by SDD. Experimentations and performances are reported on some well known examples.

Continue reading

Hierarchical set decision diagrams and automatic saturation

By Alexandre Hamez, Yann Thierry-Mieg, Fabrice Kordon

2008-03-01

In Petri nets and other models of concurrency –ICATPN 2008

Abstract

Shared decision diagram representations of a state-space have been shown to provide efficient solutions for model-checking of large systems. However, decision diagram manipulation is tricky, as the construction procedure is liable to produce intractable intermediate structures (a.k.a peak effect). The definition of the so-called saturation method has empirically been shown to mostly avoid this peak effect, and allows verification of much larger systems. However, applying this algorithm currently requires deep knowledge of the decision diagram data-structures, of the model or formalism manipulated, and a level of interaction that is not offered by the API of public DD packages. Hierarchical Set Decision Diagrams (SDD) are decision diagrams in which arcs of the structure are labeled with sets, themselves stored as SDD. This data structure offers an elegant and very efficient way of encoding structured specifications using decision diagram technology. It also offers, through the concept of inductive homomorphisms, unprecedented freedom to the user when defining the transition relation. Finally, with very limited user input, the SDD library is able to optimize evaluation of a transition relation to produce a saturation effect at runtime. We further show that using recursive folding, SDD are able to offer solutions in logarithmic complexity with respect to other DD. We conclude with some performances on well known examples.

Continue reading

libDMC: A library to operate efficient distributed model checking

By Alexandre Hamez, Fabrice Kordon, Yann Thierry-Mieg

2007-03-13

In Workshop on performance optimization for high-level languages and libraries — associated to IPDPS’2007

Abstract

Model checking is a formal verification technique that allows to automatically prove that a system’s behavior is correct. However it is often prohibitively expensive in time and memory complexity, due to the so-called state space explosion problem. We present a generic multi-threaded and distributed infrastructure library designed to allow distribution of the model checking procedure over a cluster of machines. This library is generic, and is designed to allow encapsulation of any model checker in order to make it distributed. Performance evaluations are reported and clearly show the advantages of multi-threading to occupy processors while waiting for the network, with linear speedup over the number of processors.

Continue reading

Search

Tags