CSI Seminar 2018-01-24
14h00 Efficient Translation of Fairness LTL Formulae into Deterministic Automata – Laurent XU
In the automata-theoretic approach to Linear Temporal Logic (LTL) model checking, the negation of an LTL formula is translated into an '"`UNIQ--math-00000007-QINU`"'-automaton. The construction of a smaller automaton reduces a lot the runtime and the memory consumption of the subsequent operations in the model checking pipeline. Müller and Sickert presented an efficient method to translate any LTL formula into a small deterministic automaton. This method consists in splitting the formula into three sets of subformulae which are respectively taken from the (co-)safety fragment, the fairness fragment and the rest. Then they translate all sets of subformulae apart from each other into deterministic automata and they combine these resulting automata. Spot can already translate obligation formulae into minimal deterministic automata. Since obligation formulae are a superset of (co-)safety formulae, we replace the (co-)safety fragment by the obligation fragment to generalize the translation of Müller and Sickert. Concerning the fairness fragment, they showed an efficient translation algorithm that produces small deterministic automata. They also showed a method to compute an efficient product of these automata with other automata. We present how these two methods are implemented in Spot.
14h30 Deciding Persistence or Recurrence Membership in Spot – Alexandre Gbaguidi Aïsse
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) '"`UNIQ--math-00000007-QINU`"' is recurrent (respectively persistent) is interesting because it ensures that '"`UNIQ--math-00000008-QINU`"' can be translated into a deterministic Büchi automaton (respectively into a co-Büchi automaton). Originally, Spot, a library for '"`UNIQ--math-00000009-QINU`"'-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