Working Seminar on Formal Models, Discrete Structures, and Algorithms

Ten Years of Practical Contributions to LTL and ω-Automata in Spot

Alexandre Duret-Lutz (Université Pierre & Marie Curie)

When: Monday March 20, 2pm

Where: room C417 (at the very end of the corridor)


We present multiple practical contributions to the automata-theoretic approach to LTL model checking. These have been implemented over the last 10 years in Spot (, a library and a set of tools exporting reusable algorithms, with a growing user base.

In particular, we will present an overview of the techniques used in our LTL-to-Büchi translator, that is now one of the leading tools available for this task. We will also discuss how we built algorithms that support automata with arbitrary acceptance conditions, and how it is actually easier to design a library of ω-automata with arbitrary acceptance conditions, as opposed to working with a restricted set of well known acceptance conditions such as Streett, Rabin, etc. Finally we will show how the set of tools that we have built can be used to improve existing algorithms by finding bugs or detecting nonoptimal results.