{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,12]],"date-time":"2026-09-12T05:13:22Z","timestamp":1789190002045,"version":"build-2803163510"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2024,4,10]],"date-time":"2024-04-10T00:00:00Z","timestamp":1712707200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["183790222, 317422601, and 436811179"],"award-info":[{"award-number":["183790222, 317422601, and 436811179"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"name":"European Research Council (ERC) under the European Union\u2019s Horizon 2020 research and innovation programme","award":["787367 (PaVeS)"],"award-info":[{"award-number":["787367 (PaVeS)"]}]},{"DOI":"10.13039\/501100011033","name":"Agencia Estatal de Investigaci\u00f3n","doi-asserted-by":"crossref","award":["PID2019-108528RB-C22"],"award-info":[{"award-number":["PID2019-108528RB-C22"]}],"id":[{"id":"10.13039\/501100011033","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Spanish Ministry of Universities","award":["FPU17\/02319 and EST21\/00536"],"award-info":[{"award-number":["FPU17\/02319 and EST21\/00536"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2024,4,30]]},"abstract":"<jats:p>\n            In the mid 1980s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of Linear Temporal Logic (LTL) with past operators) is equivalent to a formula of the form\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\bigwedge _{i=1}^n {\\mathbf {G}}{\\mathbf {F}}\\varphi _i \\vee {\\mathbf {F}}{\\mathbf {G}}\\psi _i\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            , where \u03c6\n            <jats:sub>\n              <jats:italic>i<\/jats:italic>\n            <\/jats:sub>\n            and \u03c8\n            <jats:sub>\n              <jats:italic>i<\/jats:italic>\n            <\/jats:sub>\n            contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalization procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present direct and purely syntactic normalization procedures for LTL, yielding a normal form very similar to the one by Chang, Manna, and Pnueli, that exhibit only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalizes the formula, translates it into a special very weak alternating automaton, and applies a simple determinization procedure, valid only for these special automata.\n          <\/jats:p>","DOI":"10.1145\/3651152","type":"journal-article","created":{"date-parts":[[2024,3,6]],"date-time":"2024-03-06T12:06:44Z","timestamp":1709726804000},"page":"1-42","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Efficient Normalization of Linear Temporal Logic"],"prefix":"10.1145","volume":"71","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9862-4919","authenticated-orcid":false,"given":"Javier","family":"Esparza","sequence":"first","affiliation":[{"name":"Technical University of Munich, Garching bei M\u00fcnchen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2983-3404","authenticated-orcid":false,"given":"Rub\u00e9n","family":"Rubio","sequence":"additional","affiliation":[{"name":"Universidad Complutense de Madrid, Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0280-8981","authenticated-orcid":false,"given":"Salomon","family":"Sickert","sequence":"additional","affiliation":[{"name":"The Hebrew University, Jerusalem, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,4,10]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","unstructured":"Tom\u00e1s Babiak Thomas Badie Alexandre Duret-Lutz Mojm\u00edr Kret\u00ednsk\u00fd and Jan Strejcek. 2013. Compositional approach to suspension and other improvements to LTL translation. In Model Checking Software. Lecture Notes in Computer Science Vol. 7976. Springer 81\u201398. 10.1007\/978-3-642-39176-7_6","DOI":"10.1007\/978-3-642-39176-7_6"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","unstructured":"Udi Boker Karoliina Lehtinen and Salomon Sickert. 2022. On the translation of automata to linear temporal logic. In Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science Vol. 13242. Springer 140\u2013160. 10.1007\/978-3-030-99253-8_8","DOI":"10.1007\/978-3-030-99253-8_8"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19600060105"},{"key":"e_1_3_3_5_2","unstructured":"Antonio Casares Thomas Colcombet and Nathana\u00ebl Fijalkow. 2021. Optimal transformations of games and automata using muller conditions. In 48th International Colloquium on Automata Languages and Programming (ICALP 2021). Leibniz International Proceedings in Informatics Vol. 198. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik Article 123 14 pages."},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","unstructured":"Antonio Casares Alexandre Duret-Lutz Klara J. Meyer Florian Renkin and Salomon Sickert. 2022. Practical applications of the alternating cycle decomposition. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science Vol. 13244. Springer 99\u2013117. 10.1007\/978-3-030-99527-0_6","DOI":"10.1007\/978-3-030-99527-0_6"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","unstructured":"Ivana Cern\u00e1 and Radek Pel\u00e1nek. 2003. Relating hierarchy of temporal properties to model checking. In Mathematical Foundations of Computer Science 2003. Lecture Notes in Computer Science Vol. 2747. Springer 318\u2013327. 10.1007\/978-3-540-45138-9_26","DOI":"10.1007\/978-3-540-45138-9_26"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","unstructured":"Edward Y. Chang Zohar Manna and Amir Pnueli. 1992. Characterization of temporal property classes. In Automata Languages and Programming. Lecture Notes in Computer Science Vol. 623. Springer 474\u2013486. 10.1007\/3-540-55719-9_97","DOI":"10.1007\/3-540-55719-9_97"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(74)80051-6"},{"key":"e_1_3_3_11_2","unstructured":"Volker Diekert and Paul Gastin. 2008. First-order definable languages. In Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas]. Texts in Logic and Games Vol. 2. Amsterdam University Press 261\u2013306."},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","unstructured":"Alexandre Duret-Lutz Etienne Renault Maximilien Colange Florian Renkin Alexandre Gbaguidi Aisse Philipp Schlehuber-Caissier Thomas Medioni Antoine Martin J\u00e9r\u00f4me Dubois Cl\u00e9ment Gillard and Henrich Lauko. 2022. From Spot 2.0 to Spot 2.10: What\u2019s new? In Computer Aided Verification. Lecture Notes in Computer Science Vol. 13372. Springer 174\u2013187. 10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3417995"},{"key":"e_1_3_3_14_2","doi-asserted-by":"crossref","unstructured":"Javier Esparza Rub\u00e9n Rubio and Salomon Sickert. 2022. A simple rewrite system for the normalization of linear temporal logic. In Principles of Systems Design. Lecture Notes in Computer Science Vol. 13660. Springer 208\u2013227.","DOI":"10.1007\/978-3-031-22337-2_10"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","unstructured":"Kousha Etessami Moshe Y. Vardi and Thomas Wilke. 1997. First-order logic with two variables and unary temporal logic. In LICS. IEEE Computer Society 228\u2013235. 10.1109\/LICS.1997.614950","DOI":"10.1109\/LICS.1997.614950"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","unstructured":"Dov M. Gabbay. 1987. The declarative past and imperative future: Executable temporal logic for interactive systems. In Temporal Logic in Specification. Lecture Notes in Computer Science Vol. 398. Springer 409\u2013448. 10.1007\/3-540-51803-7_36","DOI":"10.1007\/3-540-51803-7_36"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013976"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","unstructured":"Dov M. Gabbay Amir Pnueli Saharon Shelah and Jonathan Stavi. 1980. On the temporal analysis of fairness. In POPL. ACM Press 163\u2013173. 10.1145\/567446.567462","DOI":"10.1145\/567446.567462"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn002"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","unstructured":"Sankar Gurumurthy Orna Kupferman Fabio Somenzi and Moshe Y. Vardi. 2003. On complementing nondeterministic B\u00fcchi automata. In Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science Vol. 2860. Springer 96\u2013110. 10.1007\/978-3-540-39724-3_10","DOI":"10.1007\/978-3-540-39724-3_10"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","unstructured":"Tobias John Simon Jantsch Christel Baier and Sascha Kl\u00fcppelholz. 2021. Determinization and limit-determinization of Emerson-Lei automata. In Automated Technology for Verification and Analysis. Lecture Notes in Computer Science Vol. 12971. Springer 15\u201331. 10.1007\/978-3-030-88885-5_2","DOI":"10.1007\/978-3-030-88885-5_2"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-022-00445-7"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","unstructured":"Jan Kret\u00ednsk\u00fd Tobias Meggendorfer and Salomon Sickert. 2018. Owl: A library for \\(\\omega\\) -words automata and LTL. In Automated Technology for Verification and Analysis. Lecture Notes in Computer Science Vol. 11138. Springer 543\u2013550. 10.1007\/978-3-030-01090-4_34","DOI":"10.1007\/978-3-030-01090-4_34"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/377978.377993"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","unstructured":"Orna Lichtenstein Amir Pnueli and Lenore D. Zuck. 1985. The glory of the past. In Logic of Programs. Lecture Notes in Computer Science Vol. 193. Springer 196\u2013218. 10.1007\/3-540-15648-8_16","DOI":"10.1007\/3-540-15648-8_16"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","unstructured":"Christof L\u00f6ding and Wolfgang Thomas. 2000. Alternating automata and logics over infinite words. In Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics. Lecture Notes in Computer Science Vol. 1872. Springer 521\u2013535. 10.1007\/3-540-44929-9_36","DOI":"10.1007\/3-540-44929-9_36"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13754-9_12"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/FSCS.1990.89589"},{"key":"e_1_3_3_29_2","article-title":"On the cascaded decomposition of automata, its complexity and its application to logic","author":"Maler Oded","year":"1994","unstructured":"Oded Maler and Amir Pnueli. 1994. On the cascaded decomposition of automata, its complexity and its application to logic. Unpublished. Retrieved March 14, 2024 from http:\/\/www-verimag.imag.fr\/maler\/Papers\/decomp.pdf","journal-title":"Unpublished"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","unstructured":"Zohar Manna and Amir Pnueli. 1990. A hierarchy of temporal properties. In PODC. ACM 377\u2013410. 10.1145\/93385.93442","DOI":"10.1145\/93385.93442"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90041-Y"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"e_1_3_3_33_2","author":"McNaughton Robert","year":"1971","unstructured":"Robert McNaughton and Seymour A. Papert. 1971. Counter-Free Automata. MIT Research Monograph No. 65). MIT Press.","journal-title":"Counter-Free Automata. MIT Research Monograph No. 65)"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","unstructured":"Philipp J. Meyer Salomon Sickert and Michael Luttenberger. 2018. Strix: Explicit reactive synthesis strikes back! In Computer Aided Verification. Lecture Notes in Computer Science Vol. 10981. Springer 578\u2013586. 10.1007\/978-3-319-96145-3_31","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90049-5"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","unstructured":"David E. Muller Ahmed Saoudi and Paul E. Schupp. 1986. Alternating automata the weak monadic theory of the tree and its complexity. In Automata Languages and Programming. Lecture Notes in Computer Science Vol. 226. Springer 275\u2013283. 10.1007\/3-540-16761-7_77","DOI":"10.1007\/3-540-16761-7_77"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","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 LICS. IEEE Computer Society 422\u2013427. 10.1109\/LICS.1988.5139","DOI":"10.1109\/LICS.1988.5139"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzz081"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","unstructured":"Radek Pel\u00e1nek and Jan Strejcek. 2005. Deeper connections between LTL and alternating automata. In Implementation and Application of Automata. Lecture Notes in Computer Science Vol. 3845. Springer 238\u2013249. 10.1007\/11605157_20","DOI":"10.1007\/11605157_20"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_2"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","unstructured":"Amir Pnueli. 1977. The temporal logic of programs. In FOCS. IEEE Computer Society 46\u201357. 10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","unstructured":"Mark Reynolds. 2000. More past glories. In LICS. IEEE Computer Society 229\u2013240. 10.1109\/LICS.2000.855772","DOI":"10.1109\/LICS.2000.855772"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","unstructured":"Shmuel Safra. 1988. On the complexity of omega-automata. In FOCS. IEEE Computer Society 319\u2013327. 10.1109\/SFCS.1988.21948","DOI":"10.1109\/SFCS.1988.21948"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-10778-2"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","unstructured":"Salomon Sickert and Javier Esparza. 2020. An efficient normalization procedure for linear temporal logic and very weak alternating automata. In LICS. ACM 831\u2013844. 10.1145\/3373718.3394743","DOI":"10.1145\/3373718.3394743"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(81)90663-X"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","unstructured":"Moshe Y. Vardi. 1994. Nontraditional applications of automata theory. In Theoretical Aspects of Computer Software. Lecture Notes in Computer Science Vol. 789. Springer 575\u2013597. 10.1007\/3-540-57887-0_116","DOI":"10.1007\/3-540-57887-0_116"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","unstructured":"Moshe Y. Vardi. 1996. An automata-theoretic approach to linear temporal logic. Logics for Concurrency 226 (1996) 238\u2013266. 10.1007\/3-540-60915-6_6","DOI":"10.1007\/3-540-60915-6_6"},{"key":"e_1_3_3_50_2","volume-title":"Past Temporal Logic","author":"Zuck Lenore D.","year":"1986","unstructured":"Lenore D. Zuck. 1986. Past Temporal Logic. Ph.D. Dissertation. Weizmann Institute of Science, Israel."}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3651152","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3651152","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:49:53Z","timestamp":1750286993000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3651152"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,10]]},"references-count":49,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4,30]]}},"alternative-id":["10.1145\/3651152"],"URL":"https:\/\/doi.org\/10.1145\/3651152","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,10]]},"assertion":[{"value":"2023-01-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-04-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}