One theorem to rule them all: A unified translation of LTL into -Automata

Javier Esparza; Jan Ketínský; Salomon Sickert

doi:10.1145/3209108.3209161

One theorem to rule them all: A unified translation of LTL into -Automata

Javier Esparza, Jan Ketínský, Salomon Sickert

Technical University of Munich

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

22 Scopus citations

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

Original language	English
Title of host publication	Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	384-393
Number of pages	10
ISBN (Electronic)	9781450355834, 9781450355834
DOIs	https://doi.org/10.1145/3209108.3209161
State	Published - 9 Jul 2018
Event	33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 - Oxford, United Kingdom Duration: 9 Jul 2018 → 12 Jul 2018

Publication series

Name	Proceedings - Symposium on Logic in Computer Science
ISSN (Print)	1043-6871

Conference

Conference	33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
Country/Territory	United Kingdom
City	Oxford
Period	9/07/18 → 12/07/18

Keywords

Automata over infinite words
Deterministic automata
Linear temporal logic
Non-deterministic automata

Access to Document

10.1145/3209108.3209161

Cite this

Esparza, J., Ketínský, J., & Sickert, S. (2018). 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 (pp. 384-393). (Proceedings - Symposium on Logic in Computer Science). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1145/3209108.3209161

@inproceedings{726a3895c1d9434d9072334b261340f0,

title = "One theorem to rule them all: A unified translation of LTL into -Automata",

abstract = "We present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic B{\"u}chi automata, and nondeterministic B{\"u}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.",

keywords = "Automata over infinite words, Deterministic automata, Linear temporal logic, Non-deterministic automata",

author = "Javier Esparza and Jan Ket{\'i}nsk{\'y} and Salomon Sickert",

note = "Publisher Copyright: {\textcopyright} 2018 ACM.; 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 ; Conference date: 09-07-2018 Through 12-07-2018",

year = "2018",

month = jul,

day = "9",

doi = "10.1145/3209108.3209161",

language = "English",

series = "Proceedings - Symposium on Logic in Computer Science",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "384--393",

booktitle = "Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018",

}

Esparza, J , Ketínský, J & Sickert, S 2018, 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. Proceedings - Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers Inc., pp. 384-393, 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, United Kingdom, 9/07/18. https://doi.org/10.1145/3209108.3209161

One theorem to rule them all: A unified translation of LTL into -Automata. / Esparza, Javier ; Ketínský, Jan; Sickert, Salomon.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. Institute of Electrical and Electronics Engineers Inc., 2018. p. 384-393 (Proceedings - Symposium on Logic in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - One theorem to rule them all

T2 - 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018

AU - Esparza, Javier

AU - Ketínský, Jan

AU - Sickert, Salomon

PY - 2018/7/9

Y1 - 2018/7/9

N2 - 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.

AB - 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.

KW - Automata over infinite words

KW - Deterministic automata

KW - Linear temporal logic

KW - Non-deterministic automata

UR - http://www.scopus.com/inward/record.url?scp=85051126159&partnerID=8YFLogxK

U2 - 10.1145/3209108.3209161

DO - 10.1145/3209108.3209161

M3 - Conference contribution

AN - SCOPUS:85051126159

T3 - Proceedings - Symposium on Logic in Computer Science

SP - 384

EP - 393

BT - Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018

PB - Institute of Electrical and Electronics Engineers Inc.

Y2 - 9 July 2018 through 12 July 2018

ER -

One theorem to rule them all: A unified translation of LTL into -Automata

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this