Reactive Synthesis from LTL Specification with Spot

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 ${\displaystyle 2017}$ edition of the SYNTCOMP competition. This demonstrates the practical applicability of the parity game approach, when backed by efficient manipulations of ${\displaystyle \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.

Bibtex (lrde.bib)

@InProceedings{	  michaud.18.synt,
author	= {Thibaud Michaud and Maximilien Colange},
title		= {Reactive Synthesis from {LTL} Specification with {S}pot},
booktitle	= {Proceedings of the 7th 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.}
}