Nouvelle traduction de LTL 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
- 2010
- Numéro
- 0912
- Projects
- Spot
Résumé
Spot est une bibliothèque de model checking centrée sur l'approche automate et qui permet de vérifier des propriétés exprimées en logique temporelle à temps linéaire (LTL) sur des modèles représentés par des automates de Büchi généralisés basés sur les transitions (TGBA). Spot propose actuellement trois algorithmes pour traduire des formules LTL en TGBA, une des étapes principales de l'approche automate. Nous présentons une quatrième traduction, introduite par Tauriainen, qui utilise des automates alternants basés sur les transitions (TAA) comme représentation intermédiaire. Nous le comparerons ensuite aux trois algorithmes déjà présent dans Spot.