Réduction par simulation directe pour les TGBA

From LRDE

Revision as of 17:03, 9 January 2018 by Bot (talk | contribs) (Created page with "{{CSIReportFR | authors = Thomas Badie | titre = Réduction par simulation directe pour les TGBA | year = 2012 | resume = L'approche par automates du model checking s'appuie t...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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.