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.
--
Maximilien Colange
Assistant Professor
LRDE -- EPITA
(+33) 1 53 14 59 45
Show replies by date