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...") |
|
| (2 intermediate revisions by one other user not shown) | |
(No difference)
| |
Latest revision as of 16:40, 31 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
