English:

Spot is a model checking library centered around the automata approach, which can be used to verify properties expressed using LTL (Linear Temporal Logic) formulae on models represented as TGBA (Transition-based Generalized Büchi automata). The library offers two translation algorithms from LTL formulae into TGBA, one of the main stages of the approach. We present an extension of one of these algorithms to an extended LTL where operators are represented by finite automata, allowing Spot to verify properties that were not expressible before. We also present how we could integrate some features of PSL (Property Specification Language) in our extension.

French:

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 façons nous pourrions intérer certaines fonctionnalités de PSL (Property Specification Language) à notre extension.

* PDF : lefortier-eltl.pdf (draft)
to top