Alexandre Duret-Lutz

In Formal Methods in System Design

Abstract ltlsynt is a tool for synthesizing a reactive circuit satisfying a specification expressed as an LTL formula. ltlsynt generally follows a textbook approach: the LTL specification is translated into a parity game whose winning strategy can be seen as a Mealy machine modeling a valid controller. This article details each step of this approach, and presents various refinements integrated over the years. Some of these refinements are unique to ltlsynt: for instance, ltlsynt supports multiple ways to encode a Mealy machine as an AIG circuit, features multiple simplification algorithms for the intermediate Mealy machine, and bypasses the usual game-theoretic approach for some subclasses of LTL formulas in favor of more direct constructions.

The Mealy-machine reduction functions of Spot

By Florian Renkin, Philipp Schlehuber-Caissier, Alexandre Duret-Lutz, Adrien Pommellet

2023-07-04

In Science of Computer Programming

Abstract We present functions for reducing Mealy machines, initially detailed in our FORTE’22 article. These functions are now integrated into Spot 2.11.2, where they are used as part of the ltlsynt tool for reactive synthesis. Of course, since Spot is a library, these functions can also be used on their own, and we provide Python bindings for easy experiments. The reproducible capsule benchmarks these functions on Mealy machines from various sources, and compare them to the MeMin tool.

From Spot 2.0 to Spot 2.10: What’s new?

By Alexandre Duret-Lutz, Étienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, Henrich Lauko

2022-06-06

In Proceedings of the 34th international conference on computer aided verification (CAV’22)

Abstract Spot is a C++17 library for LTL and $\omega$-automata manipulation, with command-line utilities, and Python bindings. This paper summarizes its evolution over the past six years, since the release of Spot 2.0, which was the first version to support $\omega$-automata with arbitrary acceptance conditions, and the last version presented at a conference. Since then, Spot has been extended with several features such as acceptance transformations, alternating automata, games, LTL synthesis, and more.

The reactive synthesis competition (SYNTCOMP): 2018-2021

By Swen Jacobs, Guillermo Alberto Perez, Remco Abraham, Véronique Bruyère, Michaël Cadilhac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Klara J. Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Schlehuber-Caissier, Mouhammad Sakr, Salomon Sickert, Gaëtan Staquet, Clément Tamines, Leander Tentrup, Adam Walker

2022-06-01

In

Abstract

Effective reductions of Mealy machines

By Florian Renkin, Philipp Schlehuber-Caissier, Alexandre Duret-Lutz, Adrien Pommellet

2022-04-26

In Proceedings of the 42nd international conference on formal techniques for distributed objects, components, and systems (FORTE’22)

Abstract We revisit the problem of reducing incompletely specified Mealy machines with reactive synthesis in mind. We propose two techniques: the former is inspired by the tool MeMin and solves the minimization problem, the latter is a novel approach derived from simulation-based reductions but may not guarantee a minimized machine. However, we argue that it offers a good enough compromise between the size of the resulting Mealy machine and performance. The proposed methods are benchmarked against MeMin on a large collection of test cases made of well-known instances as well as new ones.

Practical applications of the Alternating Cycle Decomposition

By Antonio Casares, Alexandre Duret-Lutz, Klara J. Meyer, Florian Renkin, Salomon Sickert

2022-02-01

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

Abstract In 2021, Casares, Colcombet, and Fijalkow introduced the Alternating Cycle Decomposition (ACD) to study properties and transformations of Muller automata. We present the first practical implementation of the ACD in two different tools, Owl and Spot, and adapt it to the framework of Emerson-Lei automata, i.e., $\omega$-automata whose acceptance conditions are defined by Boolean formulas. The ACD provides a transformation of Emerson-Lei automata into parity automata with strong optimality guarantees: the resulting parity automaton is minimal among those automata that can be obtained by duplication of states.

Practical “paritizing” of Emerson–Lei automata

By Florian Renkin, Alexandre Duret-Lutz, Adrien Pommellet

2020-07-07

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

Abstract We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an $\omega$-automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a Transition-based Parity Automaton (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a latest appearance record principle, and introduces a partial degeneralization.

Seminator 2 can complement generalized Büchi automata via improved semi-determinization

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

2020-05-14

In Proceedings of the 32nd international conference on computer-aided verification (CAV’20)

Abstract We present the second generation of the tool Seminator that transforms transition-based generalized Büchi automata (TGBAs) into equivalent semi-deterministic automata. The tool has been extended with numerous optimizations and produces considerably smaller automata than its first version. In connection with the state-of-the-art LTL to TGBAs translator Spot, Seminator 2 produces smaller (on average) semi-deterministic automata than the direct LTL to semi-deterministic automata translator ltl2ldgba of the Owl library. Further, Seminator 2 has been extended with an improved NCSB complementation procedure for semi-deterministic automata, providing a new way to complement automata that is competitive with state-of-the-art complementation tools.

Generic emptiness check for fun and profit

By Christel Baier, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, David Müller, Jan Strejček

2019-07-29

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

Abstract We present a new algorithm for checking the emptiness of $\omega$-automata with an Emerson-Lei acceptance condition (i.e., a positive Boolean formula over sets of states or transitions that must be visited infinitely or finitely often). The algorithm can also solve the model checking problem of probabilistic positiveness of MDP under a property given as a deterministic Emerson-Lei automaton. Although both these problems are known to be NP-complete and our algorithm is exponential in general, it runs in polynomial time for simpler acceptance conditions like generalized Rabin, Streett, or parity.

Model checking with generalized Rabin and Fin-less automata

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

2019-04-01

In International Journal on Software Tools for Technology Transfer

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 a transition-based generalized Rabin automaton (TGRA), improves the model checking procedure. TGRAs can have significantly fewer states than TGBAs, however the corresponding emptiness checking procedure is more involved.

Dissecting ltlsynt

The Mealy-machine reduction functions of Spot

From Spot 2.0 to Spot 2.10: What’s new?

The reactive synthesis competition (SYNTCOMP): 2018-2021

Effective reductions of Mealy machines

Practical applications of the Alternating Cycle Decomposition

Practical “paritizing” of Emerson–Lei automata

Seminator 2 can complement generalized Büchi automata via improved semi-determinization

Generic emptiness check for fun and profit

Model checking with generalized Rabin and Fin-less automata

Search

Tags