@article{10.1145/3417995,
    Abstract = {We present a unified translation of linear temporal logic (LTL) formulas into deterministic Rabin automata (DRA), limit-deterministic B\"{u}chi automata (LDBA), and nondeterministic B\"{u}chi automata (NBA). The translations yield automata of asymptotically optimal size (double or single exponential, respectively). All three translations are derived from one single Master Theorem of purely logical nature. The Master Theorem decomposes the language of a formula into a positive Boolean combination of languages that can be translated into {$\omega$}-automata by elementary means. In particular, Safra's, ranking, and breakpoint constructions used in other translations are not needed. We further give evidence that this theoretical clean and compositional approach does not lead to large automata per se and in fact in the case of DRAs yields significantly smaller automata compared to the previously known approach using determinisation of NBAs.},
    Address = {New York, NY, USA},
    Author = {Esparza, Javier and K\v{r}et\'{\i}nsk\'{y}, Jan and Sickert, Salomon},
    File = {A Unified Translation of Linear Temporal Logic to {$\omega$}-Automata - 3417995 - a - f.pdf},
    ISSN = {0004-5411},
    Journal = {J. ACM},
    Keywords = {logic, deterministic automata, automata over infinite words, Linear temporal logic, nondeterministic automata},
    Month = {October},
    Number = {6},
    Publisher = {Association for Computing Machinery},
    Title = {A Unified Translation of Linear Temporal Logic to {$\omega$}-Automata},
    URL = {https://doi.org/10.1145/3417995},
    Volume = {67},
    Year = {2020},
    articleno = {33},
    bdsk-url-1 = {https://doi.org/10.1145/3417995},
    date-added = {2020-10-25 18:35:44 +0100},
    date-modified = {2021-02-15 10:48:22 +0100},
    issue_date = {October 2020},
    numpages = {61},
    doi = {10.1145/3417995}
}

@article{10.1145/3417995, Abstract = {We present a unified translation of linear temporal logic (LTL) formulas into deterministic Rabin automata (DRA), limit-deterministic B\"{u}chi automata (LDBA), and nondeterministic B\"{u}chi automata (NBA). The translations yield automata of asymptotically optimal size (double or single exponential, respectively). All three translations are derived from one single Master Theorem of purely logical nature. The Master Theorem decomposes the language of a formula into a positive Boolean combination of languages that can be translated into {$\omega$}-automata by elementary means. In particular, Safra's, ranking, and breakpoint constructions used in other translations are not needed. We further give evidence that this theoretical clean and compositional approach does not lead to large automata per se and in fact in the case of DRAs yields significantly smaller automata compared to the previously known approach using determinisation of NBAs.}, Address = {New York, NY, USA}, Author = {Esparza, Javier and K\v{r}et\'{\i}nsk\'{y}, Jan and Sickert, Salomon}, File = {A Unified Translation of Linear Temporal Logic to {$\omega$}-Automata - 3417995 - a - f.pdf}, ISSN = {0004-5411}, Journal = {J. ACM}, Keywords = {logic, deterministic automata, automata over infinite words, Linear temporal logic, nondeterministic automata}, Month = {October}, Number = {6}, Publisher = {Association for Computing Machinery}, Title = {A Unified Translation of Linear Temporal Logic to {$\omega$}-Automata}, URL = {https://doi.org/10.1145/3417995}, Volume = {67}, Year = {2020}, articleno = {33}, bdsk-url-1 = {https://doi.org/10.1145/3417995}, date-added = {2020-10-25 18:35:44 +0100}, date-modified = {2021-02-15 10:48:22 +0100}, issue_date = {October 2020}, numpages = {61}, doi = {10.1145/3417995} }