Deciding Persistence or Recurrence Membership in Spot

From LRDE

Revision as of 11:55, 24 January 2018 by Bot (talk | contribs) (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...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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) Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f} is recurrent (respectively persistent) is interesting because it ensures that Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f} can be translated into a deterministic Büchi automaton (respectively into a co-Büchi automaton). Originally, Spot, a library for Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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