Synthèse LTL avec 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.

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.