LTL Synthesis with Spot

From LRDE

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 Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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.