Deciding Persistence or Recurrence Membership in Spot

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) $f$ is recurrent (respectively persistent) is interesting because it ensures that $f$ can be translated into a deterministic Büchi automaton (respectively into a co-Büchi automaton). Originally, Spot, a library for $\omega$-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