by Thibaud Michaud, Maximilien Colange
Abstract:
We present \textttltlsynt, 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 \textttltlsynt 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. \textttltlsynt 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 $ømega$-automata such as the ones provided by Spot. We present our approach and report on our experimental evaluation of \textttltlsynt to better understand its strengths and weaknesses.
Reference:
Reactive Synthesis from LTL Specification with Spot (Thibaud Michaud, Maximilien Colange), In Proceedings Seventh Workshop on Synthesis, SYNT@CAV 2018, volume xx, 2018.
Bibtex Entry:
@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.}}