From LTL to deterministic automata

We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula (varphi ). The automaton is the product of a co-Büchi automaton for (varphi ) and an array of Rabin automata, one for each ({mathbf {G}})-subformula of (varphi ). The Rabin automaton for ({mathbf {G}}psi ) is in charge of recognizing whether ({mathbf {F}}{mathbf {G}}psi ) holds. This information is passed to the co-Büchi automaton that decides on acceptance. As opposed to standard procedures based on Safra’s determinization, the states of all our automata have a clear logical structure, which allows for various optimizations. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.