Tester l'appartenance à Persistence ou Récurrence dans Spot

Auteurs

Alexandre Gbaguidi Aïsse

Type

techreport

Année

2018

Numéro

1801

Résumé

Il existe une hiérarchie de propriétés temporellesdéfinie par Manna et Pnueli (1990). Cette hiérarchie contient entre autres les classes de récurrence et persistence. Savoir si une formule de logique temporelle à temps linéaire (LTL) f est récurrente (respectivement persistente) est intéressant car cela guarantit que f peut être traduit en un automate de Büchi déterministe (respectivement en un automate de co-Büchi). Auparavant, Spot, une bibliothèque de manipulation de formules LTL avait une unique façon de tester l'appartenance d'une formule aux classes de persistence ou récurrence. Grâce à nos précédents travaux présentés dans emphA co-Büching Toolbox