Alexandre Duret-Lutz

SAT-based minimization of deterministic $\omega$-automata

By Souheib Baarir, Alexandre Duret-Lutz

2015-09-01

In Proceedings of the 20th international conference on logic for programming, artificial intelligence, and reasoning (LPAR’15)

Abstract

We describe a tool that inputs a deterministic $\omega$-automaton with any acceptance condition, and synthesizes an equivalent $\omega$-automaton with another arbitrary acceptance condition and a given number of states, if such an automaton exists. This tool, that relies on a SAT-based encoding of the problem, can be used to provide minimal $\omega$-automata equivalent to given properties, for different acceptance conditions.

Continue reading

On refinement of Büchi automata for explicit model checking

By František Blahoudek, Alexandre Duret-Lutz, Vojtčech Rujbr, Jan Strejček

2015-06-15

In Proceedings of the 22th international SPIN symposium on model checking of software (SPIN’15)

Abstract

In explicit model checking, systems are typically described in an implicit and compact way. Some valid information about the system can be easily derived directly from this description, for example that some atomic propositions cannot be valid at the same time. The paper shows several ways to apply this information to improve the Büchi automaton built from an LTL specification. As a result, we get smaller automata with shorter edge labels that are easier to understand and, more importantly, for which the explicit model checking process performs better.

Continue reading

Practical stutter-invariance checks for $\omega$-regular languages

By Thibaud Michaud, Alexandre Duret-Lutz

2015-06-15

In Proceedings of the 22th international SPIN symposium on model checking of software (SPIN’15)

Abstract

We propose several automata-based constructions that check whether a specification is stutter-invariant. These constructions assume that a specification and its negation can be translated into Büchi automata, but aside from that, they are independent of the specification formalism. These transformations were inspired by a construction due to Holzmann and Kupferman, but that we broke down into two operations that can have different realizations, and that can be combined in different ways. As it turns out, implementing only one of these operations is needed to obtain a functional stutter-invariant check. Finally we have implemented these techniques in a tool so that users can easily check whether an LTL or PSL formula is stutter-invariant.

Continue reading

The Hanoi Omega-Automata format

By Tomáš Babiak, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Křetínský, David Müller, David Parker, Jan Strejček

2015-04-27

In Proceedings of the 27th international conference on computer aided verification (CAV’15)

Abstract

We propose a flexible exchange format for $\omega$-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people’s work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Büchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata.

Continue reading

Parallel explicit model checking for generalized Büchi automata

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

2015-01-13

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

Abstract

We present new parallel emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on an SCC enumeration, support generalized Buchi acceptance, and require no synchronization points nor repair procedures. A salient feature of our algorithms is the use of a global union-find data structure in which multiple threads share structural information about the automaton being checked. Our prototype implementation has encouraging performances: the new emptiness checks have better speedup than existing algorithms in half of our experiments.

Continue reading

Is there a best Büchi automaton for explicit model checking?

By František Blahoudek, Alexandre Duret-Lutz, Mojmír Křetínský, Jan Strejček

2014-06-16

In Proceedings of the 21th international SPIN symposium on model checking of software (SPIN’14)

Abstract

LTL to Büchi automata (BA) translators are traditionally optimized to produce automata with a small number of states or a small number of non-deterministic states. In this paper, we search for properties of Büchi automata that really influence the performance of explicit model checkers. We do that by manual analysis of several automata and by experiments with common LTL-to-BA translators and realistic verification tasks. As a result of these experiences, we gain a better insight into the characteristics of automata that work well with Spin.

Continue reading

A type system for weighted automata and rational expressions

By Akim Demaille, Alexandre Duret-Lutz, Sylvain Lombardy, Luca Saiu, Jacques Sakarovitch

2014-05-20

In Proceedings of implementation and application of automata, 19th international conference (CIAA’14)

Abstract

We present a type system for automata and rational expressions, expressive enough to encompass weighted automata and transducers in a single coherent formalism. The system allows to express useful properties about the applicability of operations including binary heterogeneous functions over automata. We apply the type system to the design of the platform, a library dedicated to the computation with finite weighted automata, in which genericity and high efficiency are obtained at the lowest level through the use of template metaprogramming, by letting the template system play the role of a static type system for automata. Between such a low-level layer and the interactive high-level interface, the type system plays the crucial role of a mediator and allows for a cleanly-structured use of dynamic compilation.

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

Mechanizing the minimization of deterministic generalized Büchi automata

By Souheib Baarir, Alexandre Duret-Lutz

2014-03-21

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

Abstract

Deterministic Büchi automata (DBA) are useful to (probabilistic) model checking and synthesis. We survey techniques used to obtain and minimize DBAs for different classes of properties. We extend these techniques to support DBA that have generalized and transition-based acceptance (DTGBA) as they can be even smaller. Our minimization technique—a reduction to a SAT problem—synthesizes a DTGBA equivalent to the input DTGBA for any given number of states and number of acceptance sets (assuming such automaton exists). We present benchmarks using a framework that implements all these techniques.

Continue reading

LTL translation improvements in Spot 1.0

By Alexandre Duret-Lutz

2014-03-06

In International Journal on Critical Computer-Based Systems

Abstract

Spot is a library of model-checking algorithms started in 2003. This paper focuses on its module for translating linear-time temporal logic (LTL) formulas into Büchi automata: one of the steps required in the automata-theoretic approach to LTL model-checking. We detail the different algorithms involved in this translation: the core translation itself, which performs many simplifications thanks to its use of binary decision diagrams; the pre-processing of the LTL formulas with rewriting rules chosen to help their translation; and various post-processing algorithms whose use depends on the intent of the translation: do we favor deterministic automata, or small automata? Using different benchmarks, we show how Spot competes with other LTL translators, and how it has improved over the years.

Continue reading

Search

Tags