Traduction d'une LTL étendue en TGBA dans Spot

Auteurs

Damien Lefortier

Type

techreport

Année

2009

Projects

Spot

Résumé

Spot est une bibliothèque de model checking 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 deux algorithmes de traduction de LTL en TGBA, une des étapes principales de l'approche automate. Nous présentons une nouvelle traduction en TGBA d'une LTL étendue dont les opérateurs sont représentés par des automates finis, permettant ainsi à Spot de vérifier des propriétés qui n'étaient pas exprimables auparavant. Nous présenterons aussi de quelles fac cons nous pourrions intégrer certaines fonctionnalités de PSL (Property Specification Language) à notre extension.