Le support des automates alternants

Auteurs

Amaury Fauchille

Type

techreport

Année

2016

Numéro

1612

Résumé

Les automates alternants ajoutent un branchement universel au branchement existentiel des automates non-déterministes. Les automates alternants de Büchi sont exponentiellement plus concis que les automates de Büchi non-déterministes. De plus, ils conviennent bien à la traduction de la logique temporelle linéaire car leur taille est proportionnelle à la taille de la formule traduite. Ce travail vise à ajouter le support des automates alternants à Spot. Cela rendra Spot compatible avec les outils produisant et utilisant des automates alternants, et permettra à de futurs algorithmes travaillant sur les automates alternants d'être implémentés.