@InProceedings{   michaud.18.synt,
  author        = {Thibaud Michaud and Maximilien Colange},
  title         = {Reactive Synthesis from LTL Specification with Spot},
  booktitle     = {Proceedings Seventh Workshop on Synthesis, SYNT@CAV 2018},
  series        = {Electronic Proceedings in Theoretical Computer Science},
  pages         = {xx},
  volume        = {xx},
  year          = 2018,
  abstract      = {We present \texttt{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 \texttt{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.  \texttt{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 \texttt{ltlsynt} to better understand its
                  strengths and weaknesses.}}