Efficient Translation of Fairness LTL Formulae into Deterministic Automata

From LRDE

Abstract

In the automata-theoretic approach to Linear Temporal Logic (LTL) model checking, the negation of an LTL formula is translated into an 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} -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.