LTL Synthesis with Spot

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 $\omega$-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.