Difference between revisions of "Publications/gbaguidiaisse.18.seminar"
From LRDE
(Created page with "{{CSIReport | authors = Alexandre Gbaguidi Aïsse | title = Deciding Persistence or Recurrence Membership in Spot | year = 2018 | number = 1801 | abstract = There is a hierarc...") |
|||
| Line 4: | Line 4: | ||
| year = 2018 |
| year = 2018 |
||
| number = 1801 |
| number = 1801 |
||
| − | | abstract = There is a hierarchy of temporal properties, defined by Manna and Pnueli (1990). This hierarchy contains, amongst others, the recurrence and persistence classes. Knowing that a formula of linear time temporal logic (LTL) |
+ | | abstract = There is a hierarchy of temporal properties, defined by Manna and Pnueli (1990). This hierarchy contains, amongst others, the recurrence and persistence classes. Knowing that a formula of linear time temporal logic (LTL) {{#tag:math|f}} is recurrent (respectively persistent) is interesting because it ensures that <math>f</math> can be translated into a deterministic Büchi automaton (respectively into a co-Büchi automaton). Originally, Spot, a library for <math>\omega</math>-automata manipulation, had a single way to decide if a linear temporal logic formula belongs to the recurrence or to the persistence class. Thanks to our previous work introduced in emphA co-Büching Toolbox |
| type = techreport |
| type = techreport |
||
| id = gbaguidiaisse.18.seminar |
| id = gbaguidiaisse.18.seminar |
||
Revision as of 19:10, 29 January 2018
- Authors
- Alexandre Gbaguidi Aïsse
- Type
- techreport
- Year
- 2018
- Number
- 1801
Abstract
There is a hierarchy of temporal properties, defined by Manna and Pnueli (1990). This hierarchy contains, amongst others, the recurrence and persistence classes. Knowing that a formula of linear time temporal logic (LTL) is recurrent (respectively persistent) is interesting because it ensures that can be translated into a deterministic Büchi automaton (respectively into a co-Büchi automaton). Originally, Spot, a library for -automata manipulation, had a single way to decide if a linear temporal logic formula belongs to the recurrence or to the persistence class. Thanks to our previous work introduced in emphA co-Büching Toolbox
