One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata

ESPARZA, Javier; Jan KŘETÍNSKÝ a Salomon SICKERT. One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. ACM, 2018, s. 384-393. ISBN 9781450355834. Dostupné z: https://doi.org/10.1145/3209108.3209161.

Základní údaje

Originální název

One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata

Autoři

ESPARZA, Javier; Jan KŘETÍNSKÝ a Salomon SICKERT

Vydání

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, od s. 384-393, 10 s. 2018

Nakladatel

ACM

---

Další údaje

Typ výsledku

Stať ve sborníku

Označené pro přenos do RIV

Ne

Organizační jednotka

Fakulta informatiky

ISBN

9781450355834

ISSN

DOI

https://doi.org/10.1145/3209108.3209161

---

Anotace

V originále

We present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic Büchi automata, and nondeterministic Büchi automata. 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 -automata by elementary means. In particular, Safra's, ranking, and breakpoint constructions used in other translations are not needed.