Reactive synthesis from LTL specification with Spot
In Proceedings of the 7th workshop on synthesis, SYNT@CAV 2018
Abstract We present ltlsynt, a new tool for reactive synthesis from LTL specifications. It relies on the efficiency of Spot to translate the input LTL specification to a deterministic parity automaton. The latter yields a parity game, which we solve with Zielonka’s recursive algorithm.The approach taken in ltlsynt was widely believed to be impractical, due to the double-exponential size of the parity game, and to the open status of the complexity of parity games resolution.
Derived-term automata of weighted rational expressions with quotient operators
In Proceedings of the thirteenth international colloquium on theoretical aspects of computing (ICTAC)
Abstract Quotient operators have been rarely studied in the context of weighted rational expressions and automaton generation—in spite of the key role played by the quotient of words in formal language theory. To handle both left- and right-quotients we generalize an expansion-based construction of the derived-term (or Antimirov, or equation) automaton and rely on support for a transposition (or reversal) operator. The resulting automata may have spontaneous transitions, which requires different techniques from the usual derived-term constructions.
The 4th reactive synthesis competition (SYNTCOMP 2017): Benchmarks, participants & results
In Proceedings sixth workshop on synthesis
Abstract
Spot 2.0 — a framework for LTL and $\omega$-automata manipulation
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.
Practical stutter-invariance checks for $\omega$-regular languages
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.