Tester l'appartenance à Persistence ou Récurrence 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
- 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