Réduction par simulation directe pour les TGBA

From LRDE

Résumé

L'approche par automates du model checking s'appuie traditionnellement sur des Automates de Büchi (BA) qu'on souhaite les plus petits possible. Etessami et al. ont présenté une méthode de réduction d'un BA basée sur une relation de simulation (dite directe) entre ses états. Spot, bibliothèque de model checking, utilise principalement des TGBA qui généralisent les BA. Nous montrons qu'en adaptant cette simulation aux TGBA on obtient des automates plus concis que les BA équivalents. Cette nouvelle technique est incluse dans Spot 0.9 et a permis de produire des automates plus petits que dans les précédentes versions.