Recherches de contrexemple dans Spot

Auteurs

Clément Gillard

Type

techreport

Année

2019

Numéro

1903

Résumé

Spot est une bibliothèque de manipulation d'ω-automates qui tend à aider la vérification de modèle par ω-automates et le développement d'outils de transformation d'ω-automates. Elle fournit donc de multiples algorithmes avec de multiples implémentations qui fonctionnent sur une grande variété d'ω-automates. Parmi ces algorithmesles tests de vacuité et les recherches de contrexemple sont souvent utilisés pour de diverses raisons. Comme leurs résultats sont liés, ils sont souvent utilisés ensemble. Cependant, il manque à Spot les implémentations de recherche de contrexemple correspondant à certaines implémentations de tests de vacuité qui soient capables de travailler de la même manière sur les mêmes automates. Nous présentons deux implémentations de calcul de contrexemple, qui viennent compléter deux implémentations de tests de vacuité déjà existantes, qui suivent leur sillage et se servent des données dejà accumulées pour construire efficacement des contrexemples.