LTL Synthesis with Spot
From LRDE
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
- Authors
- Thibaud Michaud
- Type
- techreport
- Year
- 2017
- Number
- 1707
Abstract
We present a new tool for circuit synthesis from LTL specifications. It reduces the synthesis problem to a parity game using Spot's efficient algorithms on -automata. Two methods have been implemented for the resolution of the game: a recent algorithm by Calude et al. which has the best known theoretical complexity for the problem, and Zielonka's recursive algorithm known for its good practical performances. Finally, the winning strategy is translated to an And-Inverter Graph that models the original LTL formula.
