LIP6 2006/003
- Rapport technique
Test de vacuité d'automates de Büchi ensemblistes en utilisant des tests d'inclusion. - S. Baarir, A. Duret-Lutz
- 18 pages - 11/10/2006- document en - http://www.lip6.fr/lip6/reports/2006/lip6-2006-003.pdf - 278 Ko
- Contact : Alexandre.Duret-Lutz (at) nulllip6.fr
- Équipe : MoVe
- Mots clés : model-checking, test de vacuité, vérification, automates de Büchi, inclusion, symétries, réduction
- Directeur de la publication : Thierry.Lanfroy (at) nulllip6.fr
Une façon de luter contre l'explosion combinatoire de l'espace d'états dans l'approche automate du model-checking est de construire un automate B dont les états représentent des ensembles d'états de l'automate original A dont on veut tester la vacuité.
Nous introduisons deux tests de vacuité pour les automates de Büchi dont les états représentent des ensembles qui peuvent s'inclure les uns les autres. Le premier test sur B équivaut au test de vacuité traditionnel que l'on ferait sur A, mais utilise des inclusions pour diriger et réduire d'avantage la construction à la volée de B. Le second test est énormément plus rapide, mais peut retourner de faux négatifs. Nous illustrons et mesurons ces deux algorithmes avec une réduction basée sur les symétries
Nous introduisons deux tests de vacuité pour les automates de Büchi dont les états représentent des ensembles qui peuvent s'inclure les uns les autres. Le premier test sur B équivaut au test de vacuité traditionnel que l'on ferait sur A, mais utilise des inclusions pour diriger et réduire d'avantage la construction à la volée de B. Le second test est énormément plus rapide, mais peut retourner de faux négatifs. Nous illustrons et mesurons ces deux algorithmes avec une réduction basée sur les symétries