Reactive Synthesis from LTL Specification with Spot

Authors

Thibaud Michaud, Maximilien Colange

Where

Proceedings of the 7th Workshop on Synthesis, SYNT@CAV 2018

Type

inproceedings

Projects

Spot

Date

2018-06-07

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.

Documents

• Paper

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.},
  nodoi		= {}
}