Recherche de chemin acceptant bi-bande dans Spot

Auteurs

Clément Gillard

Type

techreport

Année

2018

Numéro

1805

Résumé

Dans un précédent rapport nous présentions le test de vacuité bi-bande dans la bibliothèque Spot, qui vérifie que l'intersection des langages de deux ω-automates est vide sans construire leur produit, ce qui permet de contourner une limitation de Spot sur le nombre d'ensembles d'acceptations de ces automates. Cette opération, lorsque l'intersection n'est effectivement pas vide, est généralement suivie d'une recherche de chemin acceptant sur le produit qui expose un mot qui se trouve dans les langages des deux automates. Nous présentons une nouvelle fonction qui réalise cette recherche de chemin acceptant à partir des données générées par le test de vacuité bi-bande, ce qui nous permet d'utiliser ces nouvelles méthodes dans des algorithmes qui nécessitent la recherche d'un contre-exemple.