Le support des automates alternants

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é

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.