@article{Esparza:2016uj,
    Abstract = {We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula {\$}{\$}{$\backslash$}varphi {\$}{\$}. The automaton is the product of a co-B{\"u}chi automaton for {\$}{\$}{$\backslash$}varphi {\$}{\$}and an array of Rabin automata, one for each {\$}{\$}{\{}{$\backslash$}mathbf {\{}G{\}}{\}}{\$}{\$}-subformula of {\$}{\$}{$\backslash$}varphi {\$}{\$}. The Rabin automaton for {\$}{\$}{\{}{$\backslash$}mathbf {\{}G{\}}{\}}{$\backslash$}psi {\$}{\$}is in charge of recognizing whether {\$}{\$}{\{}{$\backslash$}mathbf {\{}F{\}}{\}}{\{}{$\backslash$}mathbf {\{}G{\}}{\}}{$\backslash$}psi {\$}{\$}holds. This information is passed to the co-B{\"u}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.},
    Author = {Esparza, Javier and K{\v r}et{\'\i}nsk{\'y}, Jan and Sickert, Salomon},
    File = {From LTL to deterministic automata - A safraless compositional approach - esparza2016.pdf},
    ISBN = {1572-8102},
    Journal = {Formal Methods in System Design},
    Number = {3},
    Pages = {219--271},
    Title = {From LTL to deterministic automata},
    URL = {https://doi.org/10.1007/s10703-016-0259-2},
    Volume = {49},
    Year = {2016},
    bdsk-url-1 = {https://doi.org/10.1007/s10703-016-0259-2},
    da = {2016/12/01},
    date-added = {2021-07-27 17:24:48 +0200},
    date-modified = {2021-07-27 17:24:48 +0200},
    id = {Esparza2016},
    ty = {JOUR},
    doi = {10.1007/s10703-016-0259-2}
}

@article{Esparza:2016uj, Abstract = {We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula {\$}{\$}{$\backslash$}varphi {\$}{\$}. The automaton is the product of a co-B{\"u}chi automaton for {\$}{\$}{$\backslash$}varphi {\$}{\$}and an array of Rabin automata, one for each {\$}{\$}{{}{$\backslash$}mathbf {{}G{}}{}}{\$}{\$}-subformula of {\$}{\$}{$\backslash$}varphi {\$}{\$}. The Rabin automaton for {\$}{\$}{{}{$\backslash$}mathbf {{}G{}}{}}{$\backslash$}psi {\$}{\$}is in charge of recognizing whether {\$}{\$}{{}{$\backslash$}mathbf {{}F{}}{}}{{}{$\backslash$}mathbf {{}G{}}{}}{$\backslash$}psi {\$}{\$}holds. This information is passed to the co-B{\"u}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.}, Author = {Esparza, Javier and K{\v r}et{\'\i}nsk{\'y}, Jan and Sickert, Salomon}, File = {From LTL to deterministic automata - A safraless compositional approach - esparza2016.pdf}, ISBN = {1572-8102}, Journal = {Formal Methods in System Design}, Number = {3}, Pages = {219--271}, Title = {From LTL to deterministic automata}, URL = {https://doi.org/10.1007/s10703-016-0259-2}, Volume = {49}, Year = {2016}, bdsk-url-1 = {https://doi.org/10.1007/s10703-016-0259-2}, da = {2016/12/01}, date-added = {2021-07-27 17:24:48 +0200}, date-modified = {2021-07-27 17:24:48 +0200}, id = {Esparza2016}, ty = {JOUR}, doi = {10.1007/s10703-016-0259-2} }