Test de vacuité bi-bande dans Spot

Auteurs

Clément Gillard

Type

techreport

Année

2017

Numéro

1706

Résumé

Spot est une bibliothèque qui manipule des ω-automates dont les conditions d'acceptation sont exprimées avec au plus 32 ensembles d'acceptation. Puisque la condition d'acceptation du produit de deux automates doit utiliser la somme de leurs ensembles, on ne peut pas construire des produits dont les opérandes utilisent plus de 32 ensembles au total. Une opération typique sur les automates est de calculer L(Atimes B)neemptyset pour décider si L(A) intersecte L(B). Lorsqu'elle est implémentée par empty(product(A, B))le calcul du produit limite le nombre d'ensembles d'acceptation que A et B peuvent utiliser. On propose une nouvelle fonction empty(A, B) qui réalise le test de vacuité de Atimes B sans construire un automate et donc sans limite sur les conditions d'acceptation. L'outil ltlcross peut maintenant comparer des automates pour un total supérieur á 32 ensembles d'acceptation.