@article{Esparza:2022vq,
    Abstract = {Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formula. In this paper, we describe a single exponential translation from limit-deterministic B{\"u}chi automata (LDBA) to DPA and show that it can be concatenated with a recent efficient translations from LTL to LDBA to yield a double exponential, `Safraless'LTL-to-DPA construction. We also report on an implementation and a comparison with other LTL-to-DPA translations on several sets of formulas from the literature.},
    Author = {Esparza, Javier and K{\v r}et{\'\i}nsk{\'y}, Jan and Raskin, Jean-Fran{\c c}ois and Sickert, Salomon},
    Date = {2022/07/23},
    File = {From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata - Esparza2022\_Article\_FromLinearTemporalLogicAndLimi.pdf},
    ISBN = {1433-2787},
    Journal = {International Journal on Software Tools for Technology Transfer},
    Title = {From linear temporal logic and limit-deterministic B{\"u}chi automata to deterministic parity automata},
    URL = {https://doi.org/10.1007/s10009-022-00663-1},
    Year = {2022},
    bdsk-url-1 = {https://doi.org/10.1007/s10009-022-00663-1},
    date-added = {2022-07-26 08:19:51 +0200},
    date-modified = {2022-07-26 08:19:52 +0200},
    id = {Esparza2022},
    doi = {10.1007/s10009-022-00663-1}
}

@article{Esparza:2022vq, Abstract = {Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formula. In this paper, we describe a single exponential translation from limit-deterministic B{\"u}chi automata (LDBA) to DPA and show that it can be concatenated with a recent efficient translations from LTL to LDBA to yield a double exponential, `Safraless'LTL-to-DPA construction. We also report on an implementation and a comparison with other LTL-to-DPA translations on several sets of formulas from the literature.}, Author = {Esparza, Javier and K{\v r}et{\'\i}nsk{\'y}, Jan and Raskin, Jean-Fran{\c c}ois and Sickert, Salomon}, Date = {2022/07/23}, File = {From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata - Esparza2022_Article_FromLinearTemporalLogicAndLimi.pdf}, ISBN = {1433-2787}, Journal = {International Journal on Software Tools for Technology Transfer}, Title = {From linear temporal logic and limit-deterministic B{\"u}chi automata to deterministic parity automata}, URL = {https://doi.org/10.1007/s10009-022-00663-1}, Year = {2022}, bdsk-url-1 = {https://doi.org/10.1007/s10009-022-00663-1}, date-added = {2022-07-26 08:19:51 +0200}, date-modified = {2022-07-26 08:19:52 +0200}, id = {Esparza2022}, doi = {10.1007/s10009-022-00663-1} }