Amélioration de la réduction par simulation

From LRDE

The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

Résumé

En vérification formelle à l'aide d'ω-automates, la construction d'automates plus petits réduit beaucoup le temps d'exécution et la consommation mémoire d'opérations coûteuses telles que le produit synchronisé. La minimisation d'ω-automates étant un problème NP-complet, nous concentrons notre travail sur les opérations de réduction. Spot possède déjà une méthode de réduction par simulation fonctionnant pour tous les automates existentiels ayant n'importe quelle condition d'acceptation. Cette méthode utilise une simulation à un pas reposant sur la signature des états. L. Clemente et R. Mayr proposent une méthode de réduction par simulation à n pas ne fonctionnant que pour les automates de Büchi et montrent que l'augmentation de ce nombre de pas peut améliorer la réduction. Nous essayons une généralisation de l'opération de réduction existante dans Spot pour qu'elle fonctionne avec des simulations à n pas reposant sur la signature des états. Nous présentons également comment étendre la réduction existante afin qu'elle fonctionne également pour les automates alternants.