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.

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 (geldenhuys.06.spin?). In previous work (bensalem.sumo.2011?), 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.

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.

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.

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.

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.

Continue reading

Search

Tags