Deciding Persistence or Recurrence Membership in 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.
- 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
