Alexandre Duret-Lutz

In Handbook of parallel constraint reasoning

Abstract Model checking is a fully automated, formal method for demonstrating absence of bugs in reactive systems. Here, bugs are violations of properties in Linear-time Temporal Logic (LTL). A fundamental challenge to its application is the exponential explosion in the number of system states. The current chapter discusses the use of parallelism in order to overcome this challenge. We reiterate the textbook automata-theoretic approach, which reduces the model checking problem to the graph problem of finding cycles.

Explicit state model checking with generalized büchi and rabin automata

By Vincent Bloemen, Alexandre Duret-Lutz, Jaco van de Pol

2017-05-22

In Proceedings of the 24th international SPIN symposium on model checking of software (SPIN’17)

Abstract In the automata theoretic approach to explicit state LTL model checking, the synchronized product of the model and an automaton that represents the negated formula is checked for emptiness. In practice, a (transition-based generalized) Büchi automaton (TGBA) is used for this procedure.This paper investigates whether using a more general form of acceptance, namely transition-based generalized Rabin automata (TGRAs), improves the model checking procedure. TGRAs can have significantly fewer states than TGBAs, however the corresponding emptiness checking procedure is more involved.

Seminator: A tool for semi-determinization of omega-automata

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

2017-04-03

In Proceedings of the 21th international conference on logic for programming, artificial intelligence, and reasoning (LP<AR’17)

Abstract We present a tool that transforms nondeterministic $\omega$-automata to semi-deterministic $\omega$-automata. The tool Seminator accepts transition-based generalized Büchi automata (TGBA) as an input and produces automata with two kinds of semi-determinism. The implemented procedure performs degeneralization and semi-determinization simultaneously and employs several other optimizations. We experimentally evaluate Seminator in the context of LTL to semi-deterministic automata translation.

Contributions to LTL and $\omega$-automata for model checking

By Alexandre Duret-Lutz

2017-02-01

In

Abstract

Heuristics for checking liveness properties with partial order reductions

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

2016-06-17

In Proceedings of the 14th international symposium on automated technology for verification and analysis (ATVA’16)

Abstract Checking liveness properties with partial-order reductions requires a cycle proviso to ensure that an action cannot be postponed forever. The proviso forces each cycle to contain at least one fully expanded state. We present new heuristics to select which state to expand, hoping to reduce the size of the resulting graph. The choice of the state to expand is done when encountering a dangerous edge. Almost all existing provisos expand the source of this edge, while this paper also explores the expansion of the destination and the use of SCC-based information.

Spot 2.0 — a framework for LTL and $\omega$-automata manipulation

By Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Étienne Renault, Laurent Xu

2016-06-17

In Proceedings of the 14th international symposium on automated technology for verification and analysis (ATVA’16)

Abstract We present Spot 2.0, a C++ library with Python bindings and an assortment of command-line tools designed to manipulate LTL and $\omega$-automata in batch. New automata-manipulation tools were introduced in Spot 2.0; they support arbitrary acceptance conditions, as expressible in the Hanoi Omega Automaton format. Besides being useful to researchers who have automata to process, its Python bindings can also be used in interactive environments to teach $\omega$-automata and model checking.

Variations on parallel explicit model checking for generalized Büchi automata

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

2015-10-26

In International Journal on Software Tools for Technology Transfer (STTT)

Abstract We present new parallel explicit emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on a Strongly Connected Component (SCC) enumeration, support generalized Büchi acceptance, and require no synchronization points nor recomputing 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 checked. Besides these basic algorithms, we present one architectural variant isolating threads that write to the union-find, and one extension that decomposes the automaton based on the strength of its SCCs to use more optimized emptiness checks.

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.

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.

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.

Parallel model checking algorithms for linear-time temporal logic

Explicit state model checking with generalized büchi and rabin automata

Seminator: A tool for semi-determinization of omega-automata

Contributions to LTL and $\omega$-automata for model checking

Heuristics for checking liveness properties with partial order reductions

Spot 2.0 — a framework for LTL and $\omega$-automata manipulation

Variations on parallel explicit model checking for generalized Büchi automata

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

On refinement of Büchi automata for explicit model checking

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

Search

Tags