Décomposition d'un automate de Büchi Généralisé multi-force
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.
- Auteurs
- Claire Parquier
- Type
- techreport
- Année
- 2015
- Numéro
- 1511
- Projects
- Spot
- Mots-clés
- SPOT, model checking, decomposition, Transition-based Generalized Buchi-Automata
Résumé
Les tests de vacuité permettent de savoir si le langage reconnu par un automate et vide ou non. Ces tests sont souvent utilisés dans le model checking : malheureusement, ils sont très coûteuxparticulièrement sur les automates qui ne sont ni faibles ni terminaux. Dans le but de réduire ce test coûteuxce travail implémente une option permettant d'extraire trois automates plus petits regroupant les composantes terminales, faibles et fortes de l'automate original, de facc on à ce que trois tests de vacuité correspondants puissent être effectués indépendamment en utilisant l'algorithme le plus approprié.