{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T01:19:06Z","timestamp":1790817546611,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,7,9]],"date-time":"2018-07-09T00:00:00Z","timestamp":1531094400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,7,9]]},"DOI":"10.1145\/3209108.3209161","type":"proceedings-article","created":{"date-parts":[[2018,6,27]],"date-time":"2018-06-27T08:14:43Z","timestamp":1530087283000},"page":"384-393","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["One Theorem to Rule Them All"],"prefix":"10.1145","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Salomon","family":"Sickert","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,7,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00182-4"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Tom\u00e1\u0161 Babiak Franti\u0161ek Blahoudek Alexandre Duret-Lutz Joachim Klein Jan K\u0159et\u00ednsk\u00fd David M\u00fcller David Parker and Jan Strej\u010dek. 2015. The Hanoi Omega-Automata Format. In CAV. 479--486.","DOI":"10.1007\/978-3-319-21690-4_31"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Tom\u00e1s Babiak Frantisek Blahoudek Mojm\u00edr K\u0159et\u00ednsk\u00fd and Jan Strejcek. 2013. Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F G)-Fragment. In ATVA. 24--39.","DOI":"10.1007\/978-3-319-02444-8_4"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Tom\u00e1s Babiak Mojm\u00edr K\u0159et\u00ednsk\u00fd Vojtech Reh\u00e1k and Jan Strejcek. 2012. LTL to B\u00fcchi Automata Translation: Fast and More Deterministic. In TACAS. 95--109. 10.1007\/978-3-642-28756-5_8","DOI":"10.1007\/978-3-642-28756-5_8"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1373322"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Christel Baier Stefan Kiefer Joachim Klein Sascha Kl\u00fcppelholz David M\u00fcller and James Worrell. 2016. Markov Chains and Unambiguous B\u00fcchi Automata. In CAV. 23--42.","DOI":"10.1007\/978-3-319-41528-4_2"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/321239.321249"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee Andreas Gaiser and Jan K\u0159et\u00ednsk\u00fd. 2013. Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. In CAV. 559--575.","DOI":"10.1007\/978-3-642-39799-8_37"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210339"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Jean-Michel Couvreur. 1999. On-the-Fly Verification of Linear Temporal Logic. In FM. 253--271.","DOI":"10.5555\/647544.730469"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/647768.733938"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Alexandre Duret-Lutz Alexandre Lewkowicz Amaury Fauchille Thibaud Michaud Etienne Renault and Laurent Xu. 2016. Spot 2.0 - A Framework for LTL and \u03c9-Automata Manipulation. In ATVA. 122--129.","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Javier Esparza and Jan K\u0159et\u00ednsk\u00fd. 2014. From LTL to Deterministic Automata: A Safraless Compositional Approach. In CAV. 192--208. 10.1007\/978-3-319-08867-9_13","DOI":"10.1007\/978-3-319-08867-9_13"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Javier Esparza Jan K\u0159et\u00ednsk\u00fd Jean-Fran\u00e7ois Raskin and Salomon Sickert. 2017. From LTL and Limit-Deterministic B\u00fcchi Automata to Deterministic Parity Automata. In TACAS. 426--442.","DOI":"10.1007\/978-3-662-54577-5_25"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0259-2"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209161"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/646735.701621"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","unstructured":"Carsten Fritz. 2003. Constructing B\u00fcchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating B\u00fcchi Automata. In CIAA. 35--48.","DOI":"10.5555\/1760230.1760237"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_7"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Paul Gastin and Denis Oddoux. 2001. Fast LTL to B\u00fcchi Automata Translation. In CAV. 53--65.","DOI":"10.5555\/647770.734262"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","unstructured":"Dimitra Giannakopoulou and Flavio Lerda. 2002. From States to Transitions: Improving Translation of LTL Formulae to B\u00fcchi Automata. In FORTE. 308--326.","DOI":"10.5555\/646220.682186"},{"key":"e_1_3_2_1_22_1","unstructured":"Ernst Moritz Hahn Guangyuan Li Sven Schewe Andrea Turrini and Lijun Zhang. 2015. Lazy Probabilistic Model Checking without Determinisation. In CONCUR. 354--367."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","unstructured":"Dileep Kini and Mahesh Viswanathan. 2015. Limit Deterministic and Probabilistic Automata for LTL \\ GU. In TACAS. 628--642. 10.1007\/978-3-662-46681-0_57","DOI":"10.1007\/978-3-662-46681-0_57"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Dileep Kini and Mahesh Viswanathan. 2017. Optimal Translation of LTL to Limit Deterministic Automata. In TACAS. 113--129. 10.1007\/978-3-662-54580-5_7","DOI":"10.1007\/978-3-662-54580-5_7"},{"key":"e_1_3_2_1_25_1","first-page":"235","article-title":"Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata","volume":"8837","author":"Kom\u00e1rkov\u00e1 Zuzana","year":"2014","unstructured":"Zuzana Kom\u00e1rkov\u00e1 and Jan K\u0159et\u00ednsk\u00fd. 2014. Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata. In ATVA (LNCS), Vol. 8837. 235--241.","journal-title":"ATVA (LNCS)"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Jan K\u0159et\u00ednsk\u00fd and Javier Esparza. 2012. Deterministic Automata for the (F G)-Fragment of LTL. In CAV. 7--22. 10.1007\/978-3-642-31424-7_7","DOI":"10.1007\/978-3-642-31424-7_7"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Jan K\u0159et\u00ednsk\u00fd and Rusl\u00e1n Ledesma-Garza. 2013. Rabinizer 2: Small Deterministic Automata for LTL \\ GU. In ATVA. 446--450.","DOI":"10.1007\/978-3-319-02444-8_32"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Jan K\u0159et\u00ednsk\u00fd Tobias Meggendorfer Clara Waldmann and Maximilian Weininger. 2017. Index Appearance Record for Transforming Rabin Automata into Parity Automata. In TACAS. 443--460.","DOI":"10.1007\/978-3-662-54577-5_26"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/2554641.2554657"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0442-2"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","unstructured":"Nir Piterman. 2006. From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata. In LICS. 255--264. 10.1109\/LICS.2006.28","DOI":"10.1109\/LICS.2006.28"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","unstructured":"Amir Pnueli. 1977. The Temporal Logic of Programs. In FOCS. 46--57. 10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","unstructured":"Shmuel Safra. 1988. On the Complexity of omega-Automata. In FOCS. 319--327. 10.1109\/SFCS.1988.21948","DOI":"10.1109\/SFCS.1988.21948"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Sven Schewe. 2009. Tighter Bounds for the Determinisation of B\u00fcchi Automata. In FoSSaCS. 167--181.","DOI":"10.1007\/978-3-642-00596-1_13"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Salomon Sickert Javier Esparza Stefan Jaax and Jan K\u0159et\u00ednsk\u00fd. 2016. Limit-Deterministic B\u00fcchi Automata for Linear Temporal Logic. In CAV. 312--332.","DOI":"10.1007\/978-3-319-41540-6_17"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","unstructured":"Fabio Somenzi and Roderick Bloem. 2000. Efficient B\u00fcchi Automata from LTL Formulae. In CAV. 248--263.","DOI":"10.5555\/647769.734097"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","unstructured":"Moshe Y. Vardi. 1985. Automatic Verification of Probabilistic Concurrent Finite-State Programs. In FOCS. 327--338. 10.1109\/SFCS.1985.12","DOI":"10.1109\/SFCS.1985.12"},{"key":"e_1_3_2_1_38_1","volume-title":"Vardi and Pierre Wolper","author":"Moshe","year":"1986","unstructured":"Moshe Y. Vardi and Pierre Wolper. 1986. An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report). In LICS. 332--344."}],"event":{"name":"LICS '18: 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Oxford United Kingdom","acronym":"LICS '18","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","IEEE-CS\\DATC IEEE Computer Society","EACSL European Association for Computer Science Logic"]},"container-title":["Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209161","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3209108.3209161","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:29:59Z","timestamp":1781854199000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209161"}},"subtitle":["A Unified Translation of LTL into \u03c9-Automata"],"short-title":[],"issued":{"date-parts":[[2018,7,9]]},"references-count":38,"alternative-id":["10.1145\/3209108.3209161","10.1145\/3209108"],"URL":"https:\/\/doi.org\/10.1145\/3209108.3209161","relation":{},"subject":[],"published":{"date-parts":[[2018,7,9]]},"assertion":[{"value":"2018-07-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}