{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:30:34Z","timestamp":1770287434417,"version":"3.49.0"},"reference-count":84,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2020,10,17]],"date-time":"2020-10-17T00:00:00Z","timestamp":1602892800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["317422601"],"award-info":[{"award-number":["317422601"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["787367"],"award-info":[{"award-number":["787367"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2020,12,31]]},"abstract":"<jats:p>We present a unified translation of linear temporal logic (LTL) formulas into deterministic Rabin automata (DRA), limit-deterministic B\u00fcchi automata (LDBA), and nondeterministic B\u00fcchi 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 \u03c9-automata by elementary means. In particular, Safra\u2019s, 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.<\/jats:p>","DOI":"10.1145\/3417995","type":"journal-article","created":{"date-parts":[[2020,10,17]],"date-time":"2020-10-17T22:09:06Z","timestamp":1602972546000},"page":"1-61","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["A Unified Translation of Linear Temporal Logic to \u03c9-Automata"],"prefix":"10.1145","volume":"67","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen, Garching bei M\u00fcnchen, Germany"}]},{"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen, Garching bei M\u00fcnchen, Germany"}]},{"given":"Salomon","family":"Sickert","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen, Garching bei M\u00fcnchen, Germany"}]}],"member":"320","published-online":{"date-parts":[[2020,10,17]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/963927.963928"},{"key":"#cr-split#-e_1_2_1_2_1.1","doi-asserted-by":"crossref","unstructured":"Dana Angluin and Dana Fisman. 2020. Regular -languages with an informative right congruence. Inf. Comput. (2020) 104598. DOI:https:\/\/doi.org\/10.1016\/j.ic.2020.104598 10.1016\/j.ic.2020.104598","DOI":"10.1016\/j.ic.2020.104598"},{"key":"#cr-split#-e_1_2_1_2_1.2","doi-asserted-by":"crossref","unstructured":"Dana Angluin and Dana Fisman. 2020. Regular -languages with an informative right congruence. Inf. Comput. (2020) 104598. DOI:https:\/\/doi.org\/10.1016\/j.ic.2020.104598","DOI":"10.1016\/j.ic.2020.104598"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00182-4"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_31"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-02444-8_4"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_8"},{"key":"e_1_2_1_7_1","volume-title":"Principles of Model Checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking . The MIT Press . Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. The MIT Press."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_2"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the International Conferences on Logic for Programming, Artificial Intelligence and Reasoning. 356--367","author":"Blahoudek Frantisek","year":"2017","unstructured":"Frantisek Blahoudek , Alexandre Duret-Lutz , Mikul\u00e1s Klokocka , Mojm\u00edr K\u0159et\u00ednsk\u00fd , and Jan Strejcek . 2017 . Seminator: A tool for semi-determinization of omega-automata . In Proceedings of the International Conferences on Logic for Programming, Artificial Intelligence and Reasoning. 356--367 . http:\/\/www.easychair.org\/publications\/paper\/340360. Frantisek Blahoudek, Alexandre Duret-Lutz, Mikul\u00e1s Klokocka, Mojm\u00edr K\u0159et\u00ednsk\u00fd, and Jan Strejcek. 2017. Seminator: A tool for semi-determinization of omega-automata. In Proceedings of the International Conferences on Logic for Programming, Artificial Intelligence and Reasoning. 356--367. http:\/\/www.easychair.org\/publications\/paper\/340360."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 10th International Conference on Interactive Theorem Proving, (ITP\u201919)","volume":"141","author":"Brunner Julian","year":"2019","unstructured":"Julian Brunner , Benedikt Seidl , and Salomon Sickert . 2019 . A verified and compositional translation of LTL to deterministic Rabin automata . In Proceedings of the 10th International Conference on Interactive Theorem Proving, (ITP\u201919) (LIPIcs), John Harrison, John O\u2019Leary, and Andrew Tolmach (Eds.) , Vol. 141 . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 11:1--11:19. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.11 10.4230\/LIPIcs.ITP.2019.11 Julian Brunner, Benedikt Seidl, and Salomon Sickert. 2019. A verified and compositional translation of LTL to deterministic Rabin automata. In Proceedings of the 10th International Conference on Interactive Theorem Proving, (ITP\u201919) (LIPIcs), John Harrison, John O\u2019Leary, and Andrew Tolmach (Eds.), Vol. 141. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 11:1--11:19. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.11"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/321239.321249"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55719-9_97"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_37"},{"key":"#cr-split#-e_1_2_1_14_1.1","doi-asserted-by":"crossref","unstructured":"Edmund M. Clarke Thomas A. Henzinger Helmut Veith and Roderick Bloem (Eds.). 2018. Handbook of Model Checking. Springer. DOI:https:\/\/doi.org\/10.1007\/978-3-319-10575-8 10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"#cr-split#-e_1_2_1_14_1.2","doi-asserted-by":"crossref","unstructured":"Edmund M. Clarke Thomas A. Henzinger Helmut Veith and Roderick Bloem (Eds.). 2018. Handbook of Model Checking. Springer. DOI:https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210339"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48119-2_16"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification. 249--260","author":"Daniele Marco","unstructured":"Marco Daniele , Fausto Giunchiglia , and Moshe Y. Vardi . 1999. Improved automata generation for linear temporal logic . In Proceedings of the International Conference on Computer-Aided Verification. 249--260 . Marco Daniele, Fausto Giunchiglia, and Moshe Y. Vardi. 1999. Improved automata generation for linear temporal logic. In Proceedings of the International Conference on Computer-Aided Verification. 249--260."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the ACM SIGSOFT Workshop on Formal Methods in Software Practice. 7--15","author":"Dwyer Matthew B.","unstructured":"Matthew B. Dwyer , George S. Avrunin , and James C. Corbett . 1998. Property specification patterns for finite-state verification . In Proceedings of the ACM SIGSOFT Workshop on Formal Methods in Software Practice. 7--15 . DOI:https:\/\/doi.org\/10.1145\/298595.298598 10.1145\/298595.298598 Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. 1998. Property specification patterns for finite-state verification. In Proceedings of the ACM SIGSOFT Workshop on Formal Methods in Software Practice. 7--15. DOI:https:\/\/doi.org\/10.1145\/298595.298598"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_13"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_25"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0259-2"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209161"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the International Conference on Concurrency Theory. 153--167","author":"Etessami Kousha","unstructured":"Kousha Etessami and Gerard J. Holzmann . 2000. Optimizing B\u00fcchi automata . In Proceedings of the International Conference on Concurrency Theory. 153--167 . DOI:https:\/\/doi.org\/10.1007\/3-540-44618-4_13 10.1007\/3-540-44618-4_13 Kousha Etessami and Gerard J. Holzmann. 2000. Optimizing B\u00fcchi automata. In Proceedings of the International Conference on Concurrency Theory. 153--167. DOI:https:\/\/doi.org\/10.1007\/3-540-44618-4_13"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45089-0_5"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/567446.567462"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_7"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_6"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691617_4"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 15th IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification. 3--18","author":"Gerth Rob","year":"1995","unstructured":"Rob Gerth , Doron A. Peled , Moshe Y. Vardi , and Pierre Wolper . 1995 . Simple on-the-fly automatic verification of linear temporal logic . In Proceedings of the 15th IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification. 3--18 . Rob Gerth, Doron A. Peled, Moshe Y. Vardi, and Pierre Wolper. 1995. Simple on-the-fly automatic verification of linear temporal logic. In Proceedings of the 15th IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification. 3--18."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36135-9_20"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802177"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the International Conference on Concurrency Theory (LIPIcs)","volume":"42","author":"Hahn Ernst Moritz","year":"2015","unstructured":"Ernst Moritz Hahn , Guangyuan Li , Sven Schewe , Andrea Turrini , and Lijun Zhang . 2015 . Lazy probabilistic model checking without determinisation . In Proceedings of the International Conference on Concurrency Theory (LIPIcs) , Vol. 42 . 354--367. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2015.354 10.4230\/LIPIcs.CONCUR.2015.354 Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini, and Lijun Zhang. 2015. Lazy probabilistic model checking without determinisation. In Proceedings of the International Conference on Concurrency Theory (LIPIcs), Vol. 42. 354--367. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2015.354"},{"key":"#cr-split#-e_1_2_1_34_1.1","doi-asserted-by":"crossref","unstructured":"Ernst Moritz Hahn Mateo Perez Sven Schewe Fabio Somenzi Ashutosh Trivedi and Dominik Wojtczak. 2020. Good-for-MDPs automata for probabilistic analysis and reinforcement learning. In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems Held as Part of the European Joint Conferences on Theory and Practice of Software. (Lecture Notes in Computer Science) Armin Biere and David Parker (Eds.) Vol. 12078. Springer 306--323. DOI:https:\/\/doi.org\/10.1007\/978-3-030-45190-5_17 10.1007\/978-3-030-45190-5_17","DOI":"10.1007\/978-3-030-45190-5_17"},{"key":"#cr-split#-e_1_2_1_34_1.2","doi-asserted-by":"crossref","unstructured":"Ernst Moritz Hahn Mateo Perez Sven Schewe Fabio Somenzi Ashutosh Trivedi and Dominik Wojtczak. 2020. Good-for-MDPs automata for probabilistic analysis and reinforcement learning. In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems Held as Part of the European Joint Conferences on Theory and Practice of Software. (Lecture Notes in Computer Science) Armin Biere and David Parker (Eds.) Vol. 12078. Springer 306--323. DOI:https:\/\/doi.org\/10.1007\/978-3-030-45190-5_17","DOI":"10.1007\/978-3-030-45190-5_17"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the Conference on Computer Science Logic (Lecture Notes in Computer Science)","volume":"4207","author":"Thomas","year":"1874","unstructured":"Thomas A. Henzinger and Nir Piterman. 2006. Solving games without determinization . In Proceedings of the Conference on Computer Science Logic (Lecture Notes in Computer Science) , Vol. 4207 . Springer, 395--410. DOI:https:\/\/doi.org\/10.1007\/1 1874 683_26 10.1007\/11874683_26 Thomas A. Henzinger and Nir Piterman. 2006. Solving games without determinization. In Proceedings of the Conference on Computer Science Logic (Lecture Notes in Computer Science), Vol. 4207. Springer, 395--410. DOI:https:\/\/doi.org\/10.1007\/11874683_26"},{"key":"e_1_2_1_36_1","volume-title":"In Proceedings of the 5th Reactive Synthesis Competition (SYNTCOMP\u201918)","author":"Jacobs Swen","year":"2019","unstructured":"Swen Jacobs , Roderick Bloem , Maximilien Colange , Peter Faymonville , Bernd Finkbeiner , Ayrat Khalimov , Felix Klein , Michael Luttenberger , Philipp J. Meyer , Thibaud Michaud , Mouhammad Sakr , Salomon Sickert , Leander Tentrup , and Adam Walker . 2019 . In Proceedings of the 5th Reactive Synthesis Competition (SYNTCOMP\u201918) : Benchmarks, Participants 8 Results. CoRR abs\/ 1904.07736 (2019). Swen Jacobs, Roderick Bloem, Maximilien Colange, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Philipp J. Meyer, Thibaud Michaud, Mouhammad Sakr, Salomon Sickert, Leander Tentrup, and Adam Walker. 2019. In Proceedings of the 5th Reactive Synthesis Competition (SYNTCOMP\u201918): Benchmarks, Participants 8 Results. CoRR abs\/1904.07736 (2019)."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_17"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_57"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_7"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.022"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6_17"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_24"},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the ACM\/IEEE Symposium on Logic in Computer Science. 81--92","author":"Kupferman Orna","year":"1998","unstructured":"Orna Kupferman and Moshe Y. Vardi . 1998. Freedom, weakness, and determinism: From linear-time to branching-time . In Proceedings of the ACM\/IEEE Symposium on Logic in Computer Science. 81--92 . DOI:https:\/\/doi.org\/10.1109\/LICS. 1998 .705645 10.1109\/LICS.1998.705645 Orna Kupferman and Moshe Y. Vardi. 1998. Freedom, weakness, and determinism: From linear-time to branching-time. In Proceedings of the ACM\/IEEE Symposium on Logic in Computer Science. 81--92. DOI:https:\/\/doi.org\/10.1109\/LICS.1998.705645"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_7"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-02444-8_32"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_34"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_30"},{"key":"e_1_2_1_49_1","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 443--460","author":"K\u0159et\u00ednsk\u00fd Jan","year":"2017","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 Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 443--460 . DOI:https:\/\/doi.org\/10.1007\/978-3-662-54577-5_26 10.1007\/978-3-662-54577-5_26 Jan K\u0159et\u00ednsk\u00fd, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. 2017. Index appearance record for transforming Rabin automata into parity automata. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 443--460. DOI:https:\/\/doi.org\/10.1007\/978-3-662-54577-5_26"},{"key":"e_1_2_1_50_1","series-title":"Lecture Notes in Computer Science","volume-title":"Theories of Programming and Formal Methods\u2014Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, Zhiming Liu, Jim Woodcock, and Huibiao Zhu (Eds.)","author":"Li Jianwen","unstructured":"Jianwen Li , Geguang Pu , Lijun Zhang , Zheng Wang , Jifeng He , and Kim Guldstrand Larsen . 2013. On the relationship between LTL normal forms and B\u00fcchi automata . In Theories of Programming and Formal Methods\u2014Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, Zhiming Liu, Jim Woodcock, and Huibiao Zhu (Eds.) . Lecture Notes in Computer Science , Vol. 8051 . Springer , 256--270. DOI:https:\/\/doi.org\/10.1007\/978-3-642-39698-4_16 10.1007\/978-3-642-39698-4_16 Jianwen Li, Geguang Pu, Lijun Zhang, Zheng Wang, Jifeng He, and Kim Guldstrand Larsen. 2013. On the relationship between LTL normal forms and B\u00fcchi automata. In Theories of Programming and Formal Methods\u2014Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, Zhiming Liu, Jim Woodcock, and Huibiao Zhu (Eds.). Lecture Notes in Computer Science, Vol. 8051. Springer, 256--270. DOI:https:\/\/doi.org\/10.1007\/978-3-642-39698-4_16"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0442-2"},{"key":"e_1_2_1_52_1","volume-title":"Methods for the Transformation of Automata: Complexity and Connection to Second Order Logic. Master\u2019s thesis","author":"L\u00f6ding Christoph","unstructured":"Christoph L\u00f6ding . 1999. Methods for the Transformation of Automata: Complexity and Connection to Second Order Logic. Master\u2019s thesis . Institute of Computer Science and Applied Mathematics, Christian-Albrechts-University of Kiel , Germany. Christoph L\u00f6ding. 1999. Methods for the Transformation of Automata: Complexity and Connection to Second Order Logic. Master\u2019s thesis. Institute of Computer Science and Applied Mathematics, Christian-Albrechts-University of Kiel, Germany."},{"key":"e_1_2_1_53_1","volume-title":"Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, (LIPIcs), Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi (Eds.)","volume":"132","author":"L\u00f6ding Christof","year":"2019","unstructured":"Christof L\u00f6ding and Anton Pirogov . 2019 . Determinization of B\u00fcchi automata: Unifying the approaches of Safra and Muller-Schupp . In Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, (LIPIcs), Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi (Eds.) , Vol. 132 . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 120:1--120:13. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.ICALP. 2019.120 10.4230\/LIPIcs.ICALP.2019.120 Christof L\u00f6ding and Anton Pirogov. 2019. Determinization of B\u00fcchi automata: Unifying the approaches of Safra and Muller-Schupp. In Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, (LIPIcs), Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi (Eds.), Vol. 132. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 120:1--120:13. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2019.120"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_18"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-019-00349-3"},{"key":"e_1_2_1_56_1","volume-title":"Proceedings of the ACM Symposium on Principles of Distributed Computing. 377--410","author":"Manna Zohar","year":"1990","unstructured":"Zohar Manna and Amir Pnueli . 1990 . A hierarchy of temporal properties . In Proceedings of the ACM Symposium on Principles of Distributed Computing. 377--410 . DOI:https:\/\/doi.org\/10.1145\/93385.93442 10.1145\/93385.93442 Zohar Manna and Amir Pnueli. 1990. A hierarchy of temporal properties. In Proceedings of the ACM Symposium on Principles of Distributed Computing. 377--410. DOI:https:\/\/doi.org\/10.1145\/93385.93442"},{"key":"e_1_2_1_57_1","volume-title":"Strix: Explicit reactive synthesis strikes back! In Proceedings of the International Conference on Computer-Aided Verification. 578--586. DOI:https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31","author":"Meyer Philipp J.","year":"2018","unstructured":"Philipp J. Meyer , Salomon Sickert , and Michael Luttenberger . 2018 . Strix: Explicit reactive synthesis strikes back! In Proceedings of the International Conference on Computer-Aided Verification. 578--586. DOI:https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31 10.1007\/978-3-319-96145-3_31 Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. 2018. Strix: Explicit reactive synthesis strikes back! In Proceedings of the International Conference on Computer-Aided Verification. 578--586. DOI:https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90049-5"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.256.13"},{"key":"e_1_2_1_60_1","volume-title":"Proceedings of the ACM\/IEEE Symposium on Logic in Computer Science. 422--427","author":"Muller David E.","year":"1988","unstructured":"David E. Muller , Ahmed Saoudi , and Paul E. Schupp . 1988. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time . In Proceedings of the ACM\/IEEE Symposium on Logic in Computer Science. 422--427 . DOI:https:\/\/doi.org\/10.1109\/LICS. 1988 .5139 10.1109\/LICS.1988.5139 David E. Muller, Ahmed Saoudi, and Paul E. Schupp. 1988. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In Proceedings of the ACM\/IEEE Symposium on Logic in Computer Science. 422--427. DOI:https:\/\/doi.org\/10.1109\/LICS.1988.5139"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.28"},{"key":"e_1_2_1_62_1","volume-title":"From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Log. Meth. Comput. Sci. 3, 3","author":"Piterman Nir","year":"2007","unstructured":"Nir Piterman . 2007. From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Log. Meth. Comput. Sci. 3, 3 ( 2007 ). DOI:https:\/\/doi.org\/10.2168\/LMCS-3(3:5)2007 10.2168\/LMCS-3(3:5)2007 Nir Piterman. 2007. From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Log. Meth. Comput. Sci. 3, 3 (2007). DOI:https:\/\/doi.org\/10.2168\/LMCS-3(3:5)2007"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1988.21948"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00596-1_13"},{"key":"e_1_2_1_68_1","volume-title":"Linear temporal logic. Arch. Form. Proofs","author":"Sickert Salomon","year":"2016","unstructured":"Salomon Sickert . 2016. Linear temporal logic. Arch. Form. Proofs 2016 . Retrieved from https:\/\/www.isa-afp.org\/entries\/LTL.shtml. Salomon Sickert. 2016. Linear temporal logic. Arch. Form. Proofs 2016. Retrieved from https:\/\/www.isa-afp.org\/entries\/LTL.shtml."},{"key":"#cr-split#-e_1_2_1_70_1.1","unstructured":"Salomon Sickert. 2020. A Unified Translation of Linear Temporal Logic to -Automata: Supplemental Material for the Experimental Evaluation. DOI:https:\/\/doi.org\/10.5281\/zenodo.3972121 10.5281\/zenodo.3972121"},{"key":"#cr-split#-e_1_2_1_70_1.2","unstructured":"Salomon Sickert. 2020. A Unified Translation of Linear Temporal Logic to -Automata: Supplemental Material for the Experimental Evaluation. DOI:https:\/\/doi.org\/10.5281\/zenodo.3972121"},{"key":"e_1_2_1_71_1","volume-title":"Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller (Eds.). ACM, 831--844","author":"Sickert Salomon","year":"2020","unstructured":"Salomon Sickert and Javier Esparza . 2020 . An efficient normalisation procedure for linear temporal logic and very weak alternating automata . In Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller (Eds.). ACM, 831--844 . DOI:https:\/\/doi.org\/10.1145\/3373718.3394743 10.1145\/3373718.3394743 Salomon Sickert and Javier Esparza. 2020. An efficient normalisation procedure for linear temporal logic and very weak alternating automata. In Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller (Eds.). ACM, 831--844. DOI:https:\/\/doi.org\/10.1145\/3373718.3394743"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_17"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_9"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211865"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_21"},{"key":"e_1_2_1_76_1","volume-title":"Proceedings of the International Colloquium on Theoretical Aspects of Computing. 11--34","author":"Sulzmann Martin","year":"2018","unstructured":"Martin Sulzmann and Peter Thiemann . 2018 . LTL semantic tableaux and alternating -automata via linear factors . In Proceedings of the International Colloquium on Theoretical Aspects of Computing. 11--34 . DOI:https:\/\/doi.org\/10.1007\/978-3-030-02508-3_2 10.1007\/978-3-030-02508-3_2 Martin Sulzmann and Peter Thiemann. 2018. LTL semantic tableaux and alternating -automata via linear factors. In Proceedings of the International Colloquium on Theoretical Aspects of Computing. 11--34. DOI:https:\/\/doi.org\/10.1007\/978-3-030-02508-3_2"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0139-8"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1985.12"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57887-0_116"},{"key":"e_1_2_1_80_1","volume-title":"Proceedings of the Symposium on Logic in Computer Science. IEEE Computer Society, 332--344","author":"Moshe","unstructured":"Moshe Y. Vardi and Pierre Wolper. 1986. An automata-theoretic approach to automatic program verification (preliminary report) . In Proceedings of the Symposium on Logic in Computer Science. IEEE Computer Society, 332--344 . Moshe Y. Vardi and Pierre Wolper. 1986. An automata-theoretic approach to automatic program verification (preliminary report). In Proceedings of the Symposium on Logic in Computer Science. IEEE Computer Society, 332--344."},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(86)90026-7"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3417995","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3417995","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:35Z","timestamp":1750195895000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3417995"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,17]]},"references-count":84,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,12,31]]}},"alternative-id":["10.1145\/3417995"],"URL":"https:\/\/doi.org\/10.1145\/3417995","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,10,17]]},"assertion":[{"value":"2020-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-10-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}