Difference between revisions of "Publications/gbaguidiaisse.18.seminar/fr"
From LRDE
(Created page with "{{CSIReportFR | authors = Alexandre Gbaguidi Aïsse | titre = Tester l'appartenance à Persistence ou Récurrence dans Spot | year = 2018 | number = 1801 | resume = Il existe ...") |
|||
| Line 4: | Line 4: | ||
| year = 2018 |
| year = 2018 |
||
| number = 1801 |
| number = 1801 |
||
| − | | resume = 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, |
+ | | resume = 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 |
| type = techreport |
| type = techreport |
||
| id = gbaguidiaisse.18.seminar |
| id = gbaguidiaisse.18.seminar |
||
Latest revision as of 12:44, 27 February 2018
- 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