19 citations · 25 across the 10 of their papers we have counts for
5 papers · 1 filter
Teaching LTL and ω-automata with Spot
Alexandre Duret-Lutz
Spot is a mature, open-source C++/Python library and toolset for Linear Temporal Logic (LTL) and -automata manipulation. While Spot is routinely used as a research and verificat…
On-the-fly LTLf Synthesis under Partial Observability
Nadav Alon, Supratik Chakraborty, Alexandre Duret-Lutz +4
LTLf synthesis under partial observability requires reasoning about unobservable environment variables, which is typically handled by constructing a belief-state DFA via subset con…
From Spot 2.0 to Spot 2.10: What's New?
Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange +8
Spot is a C ++ 17 library for LTL and -automata manipulation, with command-line utilities, and Python bindings. This paper summarizes its evolution over the past six years, sinc…
The Reactive Synthesis Competition (SYNTCOMP): 2018-2021
Swen Jacobs, Guillermo A. Perez, Remco Abraham +22
We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Th…
Combining Explicit and Symbolic Approaches for Better On-the-Fly LTL Model Checking
Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud +1
We present two new hybrid techniques that replace the synchronized product used in the automata-theoretic approach for LTL model checking. The proposed products are explicit graphs…