Produit d'automates à parité

Auteurs

Laurent Xu

Type

techreport

Année

2016

Numéro

1607

Résumé

Spot, une bibliothèque manipulant les ω-automates basés sur les transitions, offre une méthode qui construit des automates à parité déterministes à partir d'automates de Büchi non-déterministes. Nous présentons trois outils qui manipulent les automates avec une condition d'acceptation à parité. Ces outils sont la réduction du nombre d'ensembles dans la condition d'acceptation, la modification du style de la condition d'acceptation et la coloration d'un automate. Olivier Carton a présenté une méthode pour constuire le produit d'automates à parité basés sur les étatsqui conserve la parité. Nous adaptons cette méthode afin qu'elle fonctionne également avec des automates basés sur les transitions, puis nous présentons des optimisations de ce produit. Notre travail offre un meilleur support des automates avec une conditions d'acceptation à parité. Il pourrait également permettre d'optimiser la déterminisation d'automates de Büchi.