FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
One Theorem to Rule Them All: A Unified Translation of LTL into $\omega$-Automata

Authors: Javier Esparza, Jan Kretinsky and Salomon Sickert

Paper Information

Title:One Theorem to Rule Them All: A Unified Translation of LTL into $\omega$-Automata
Authors:Javier Esparza, Jan Kretinsky and Salomon Sickert
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:Linear Temporal Logic, Automata over infinite words, Deterministic Automata, Non-Deterministic Automata
Abstract:

ABSTRACT. 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 $\omega$-automata by elementary means. In particular, the breakpoint, Safra, and ranking constructions used in other translations are not needed.

Pages:10
Talk:Jul 09 16:00 (Session 51D)
Paper: