LTL Synthesis with Spot
- Thibaud Michaud
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.