Traduction d'une LTL étendue en TGBA dans Spot

From LRDE

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.