Greetings,

We are pleased to announce that the following article has been accepted for publication in the 7th Workshop on Synthesis (SYNT@CAV 2018), to be held in Oxford on July, 18th 2018.

"Reactive Synthesis from LTL Specification with Spot"     Thibaud Michaud        (LRDE -- EPITA)     Maximilien Colange    (LRDE -- EPITA)

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. ltlsynt ranked second of its track in the 2017 edition of the SYNTCOMP competition. This demonstrates the practical applicability of the parity game approach, when backed by efficient manipulations of omega-automata such as the ones provided by Spot. We present our approach and report on our experimental evaluation of ltlsynt to better understand its strengths and weaknesses.