Reactive Synthesis from LTL Specification with Spot

From LRDE

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

Documents

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.}
}