From LTL to deterministic automata
We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula \varphi $ph. The automaton is the product of a co Buchi automaton for \varphi $ph and an array of Rabin automata, one for each \mathbf {G}$G subformula of \varphi $ph. The Rabin automaton for \mathbf {G}\psi $Gps is in charge of recognizing whether \mathbf {F}\mathbf {G}\psi $FGps holds. This information is passed to the co Buchi 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.
Formal Methods Syst. Des.