Traduction d'une LTL étendue en TGBA dans Spot
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
- Damien Lefortier
- Type
- techreport
- Année
- 2008
- Numéro
- 0807
- Projects
- Spot
Résumé
Spot repose sur l'approche automate du emphmodel checking. La bibliothèque permet de vérifier des propriétés exprimées en logique temporelle à temps linéaire (LTL) sur une modélisation d'un système représentée par un automate de Büchi généralisé basé sur les transitions (TGBA). Spot propose actuellement deux algorithmes de traduction de LTL en TGBAune des deux étapes principales de l'approche automate. Nous présentons une nouvelle traduction en TGBA d'une logique LTL qui a été étendue en y ajoutant des opérateurs représentés par des automates finis. Cette traduction permet à Spot de vérifier des propriétés qui n'étaient pas exprimables auparavant.