Synthèse LTL avec Spot

Auteurs

Thibaud Michaud

Type

techreport

Année

2017

Numéro

1707

Résumé

Nous présentons un nouvel outil de synthèse de circuit à partir de spécifications LTL. Il réduit le problème de synthèse à un jeu à parité en exploitant la bibliothèque Spot pour manipuler efficacement les ω-automates. Deux méthodes ont été implémentées pour la résolution du jeu: l'algorithme récemment découvert par Calude et al., qui a la meilleure compléxité théorique connue pour ce problème, et l'algorithme récursif de Zielonka, connu pour ses bonnes performances pratique. Finalement, la stratégie gagnante est traduite en un circuit Et-Inverseur qui modélise la formule LTL d'origine.