Difference between revisions of "Publications/michaud.18.synt"
From LRDE
| Line 4: | Line 4: | ||
| authors = Thibaud Michaud, Maximilien Colange |
| authors = Thibaud Michaud, Maximilien Colange |
||
| title = Reactive Synthesis from LTL Specification with Spot |
| title = Reactive Synthesis from LTL Specification with Spot |
||
| − | | booktitle = Proceedings |
+ | | booktitle = Proceedings of the 7th Workshop on Synthesis, SYNT@CAV 2018 |
| series = Electronic Proceedings in Theoretical Computer Science |
| series = Electronic Proceedings in Theoretical Computer Science |
||
| pages = xx |
| pages = xx |
||
| Line 17: | Line 17: | ||
@InProceedings<nowiki>{</nowiki> michaud.18.synt, |
@InProceedings<nowiki>{</nowiki> michaud.18.synt, |
||
author = <nowiki>{</nowiki>Thibaud Michaud and Maximilien Colange<nowiki>}</nowiki>, |
author = <nowiki>{</nowiki>Thibaud Michaud and Maximilien Colange<nowiki>}</nowiki>, |
||
| − | title = <nowiki>{</nowiki>Reactive Synthesis from <nowiki>{</nowiki>LTL<nowiki>}</nowiki> Specification with |
+ | title = <nowiki>{</nowiki>Reactive Synthesis from <nowiki>{</nowiki>LTL<nowiki>}</nowiki> Specification with <nowiki>{</nowiki>S<nowiki>}</nowiki>pot<nowiki>}</nowiki>, |
| − | booktitle = <nowiki>{</nowiki>Proceedings |
+ | booktitle = <nowiki>{</nowiki>Proceedings of the 7th Workshop on Synthesis, SYNT@CAV |
| + | 2018<nowiki>}</nowiki>, |
||
series = <nowiki>{</nowiki>Electronic Proceedings in Theoretical Computer Science<nowiki>}</nowiki>, |
series = <nowiki>{</nowiki>Electronic Proceedings in Theoretical Computer Science<nowiki>}</nowiki>, |
||
pages = <nowiki>{</nowiki>xx<nowiki>}</nowiki>, |
pages = <nowiki>{</nowiki>xx<nowiki>}</nowiki>, |
||
Revision as of 15:17, 29 October 2018
- 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 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.}
}