From LTL to Deterministic Automata: A Safraless Compositional Approach

Javier Esparza, Jan Křetínský

We present a new algorithm to construct a deterministic Rabin automaton for an LTL formula $\phi$. The automaton is the product of a master automaton and an array of slave automata, o…