{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,14]],"date-time":"2026-04-14T15:47:41Z","timestamp":1776181661630,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T00:00:00Z","timestamp":1594166400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["787367"],"award-info":[{"award-number":["787367"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]},{"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"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,7,8]]},"DOI":"10.1145\/3373718.3394743","type":"proceedings-article","created":{"date-parts":[[2020,5,26]],"date-time":"2020-05-26T00:23:18Z","timestamp":1590452598000},"page":"831-844","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata"],"prefix":"10.1145","author":[{"given":"Salomon","family":"Sickert","sequence":"first","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"10th International Conference on Interactive Theorem Proving, ITP 2019","volume":"19","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 10th International Conference on Interactive Theorem Proving, ITP 2019 , September 9 --12 , 2019, Portland, OR, USA (LIPIcs, Vol. 141), John Harrison, John O'Leary, and Andrew Tolmach (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 11:1--11: 19 . 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 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9--12, 2019, Portland, OR, USA (LIPIcs, Vol. 141), John Harrison, John O'Leary, and Andrew Tolmach (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 11:1--11:19. https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.11"},{"key":"e_1_3_2_1_2_1","volume-title":"28th International Symposium, MFCS 2003, Bratislava, Slovakia, August 25-29, 2003, Proceedings (Lecture Notes in Computer Science","volume":"327","author":"\u010cern\u00e1 Ivana","year":"2003","unstructured":"Ivana \u010cern\u00e1 and Radek Pel\u00e1nek . 2003 . Relating Hierarchy of Temporal Properties to Model Checking. In Mathematical Foundations of Computer Science 2003 , 28th International Symposium, MFCS 2003, Bratislava, Slovakia, August 25-29, 2003, Proceedings (Lecture Notes in Computer Science , Vol. 2747), Branislav Rovan and Peter Vojt\u00e1s (Eds.). Springer, 318-- 327 . https:\/\/doi.org\/10.1007\/978-3-540-45138-9_26 10.1007\/978-3-540-45138-9_26 Ivana \u010cern\u00e1 and Radek Pel\u00e1nek. 2003. Relating Hierarchy of Temporal Properties to Model Checking. In Mathematical Foundations of Computer Science 2003, 28th International Symposium, MFCS 2003, Bratislava, Slovakia, August 25-29, 2003, Proceedings (Lecture Notes in Computer Science, Vol. 2747), Branislav Rovan and Peter Vojt\u00e1s (Eds.). Springer, 318--327. https:\/\/doi.org\/10.1007\/978-3-540-45138-9_26"},{"key":"e_1_3_2_1_3_1","volume-title":"19th International Colloquium, ICALP92","volume":"486","author":"Chang Edward Y.","year":"1992","unstructured":"Edward Y. Chang , Zohar Manna , and Amir Pnueli . 1992 . Characterization of Temporal Property Classes. In Automata, Languages and Programming , 19th International Colloquium, ICALP92 , Vienna, Austria , July 13-17, 1992, Proceedings (Lecture Notes in Computer Science, Vol. 623), Werner Kuich (Ed.). Springer, 474-- 486 . https:\/\/doi.org\/10.1007\/3-540-55719-9_97 10.1007\/3-540-55719-9_97 Edward Y. Chang, Zohar Manna, and Amir Pnueli. 1992. Characterization of Temporal Property Classes. In Automata, Languages and Programming, 19th International Colloquium, ICALP92, Vienna, Austria, July 13-17, 1992, Proceedings (Lecture Notes in Computer Science, Vol. 623), Werner Kuich (Ed.). Springer, 474--486. https:\/\/doi.org\/10.1007\/3-540-55719-9_97"},{"key":"e_1_3_2_1_4_1","volume-title":"Corbett","author":"Dwyer Matthew B.","year":"1998","unstructured":"Matthew B. Dwyer , George S. Avrunin , and James C . Corbett . 1998 . Property specification patterns for finite-state verification. In FMSP. 7--15. 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 FMSP. 7--15. https:\/\/doi.org\/10.1145\/298595.298598"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209161"},{"key":"e_1_3_2_1_6_1","volume-title":"CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings (Lecture Notes in Computer Science","volume":"110","author":"Gurumurthy Sankar","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, 12th IFIP WG 10.5 Advanced Research Working Conference , CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings (Lecture Notes in Computer Science , Vol. 2860), Daniel Geist and Enrico Tronci (Eds.). Springer, 96-- 110 . https:\/\/doi.org\/10.1007\/978-3-540-39724-3_10 10.1007\/978-3-540-39724-3_10 Sankar Gurumurthy, Orna Kupferman, Fabio Somenzi, and Moshe Y. Vardi. 2003. On Complementing Nondeterministic B\u00fcchi Automata. In Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings (Lecture Notes in Computer Science, Vol. 2860), Daniel Geist and Enrico Tronci (Eds.). Springer, 96--110. https:\/\/doi.org\/10.1007\/978-3-540-39724-3_10"},{"key":"e_1_3_2_1_7_1","volume-title":"ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings (Lecture Notes in Computer Science","volume":"550","author":"Kret\u00ednsk\u00fd Jan","year":"2018","unstructured":"Jan Kret\u00ednsk\u00fd , Tobias Meggendorfer , and Salomon Sickert . 2018 . Owl: A Library for \u03c9-Words, Automata, and LTL. In Automated Technology for Verification and Analysis - 16th International Symposium , ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings (Lecture Notes in Computer Science , Vol. 11138), Shuvendu K. Lahiri and Chao Wang (Eds.). Springer, 543-- 550 . https:\/\/doi.org\/10.1007\/978-3-030-01090-4_34 10.1007\/978-3-030-01090-4_34 Jan Kret\u00ednsk\u00fd, Tobias Meggendorfer, and Salomon Sickert. 2018. Owl: A Library for \u03c9-Words, Automata, and LTL. In Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 11138), Shuvendu K. Lahiri and Chao Wang (Eds.). Springer, 543--550. https:\/\/doi.org\/10.1007\/978-3-030-01090-4_34"},{"key":"e_1_3_2_1_8_1","volume-title":"Conference","author":"Lichtenstein Orna","year":"1985","unstructured":"Orna Lichtenstein , Amir Pnueli , and Lenore D. Zuck . 1985. The Glory of the Past. In Logics of Programs , Conference , Brooklyn College, New York, NY, USA , June 17-19, 1985 , Proceedings (Lecture Notes in Computer Science, Vol. 193), Rohit Parikh (Ed.). Springer, 196--218. https:\/\/doi.org\/10.1007\/3-540-15648-8_16 10.1007\/3-540-15648-8_16 Orna Lichtenstein, Amir Pnueli, and Lenore D. Zuck. 1985. The Glory of the Past. In Logics of Programs, Conference, Brooklyn College, New York, NY, USA, June 17-19, 1985, Proceedings (Lecture Notes in Computer Science, Vol. 193), Rohit Parikh (Ed.). Springer, 196--218. https:\/\/doi.org\/10.1007\/3-540-15648-8_16"},{"key":"e_1_3_2_1_9_1","volume-title":"International Conference IFIP TCS 2000, Sendai, Japan, August 17-19, 2000, Proceedings (Lecture Notes in Computer Science","volume":"535","author":"L\u00f6ding Christof","year":"2000","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 , International Conference IFIP TCS 2000, Sendai, Japan, August 17-19, 2000, Proceedings (Lecture Notes in Computer Science , Vol. 1872), Jan van Leeuwen, Osamu Watanabe, Masami Hagiya, Peter D. Mosses, and Takayasu Ito (Eds.). Springer, 521-- 535 . https:\/\/doi.org\/10.1007\/3-540-44929--9_36 10.1007\/3-540-44929--9_36 Christof L\u00f6ding and Wolfgang Thomas. 2000. Alternating Automata and Logics over Infinite Words. In Theoretical Computer Science, Exploring New Frontiers of Theoretical Informatics, International Conference IFIP TCS 2000, Sendai, Japan, August 17-19, 2000, Proceedings (Lecture Notes in Computer Science, Vol. 1872), Jan van Leeuwen, Osamu Watanabe, Masami Hagiya, Peter D. Mosses, and Takayasu Ito (Eds.). Springer, 521--535. https:\/\/doi.org\/10.1007\/3-540-44929--9_36"},{"key":"e_1_3_2_1_10_1","volume-title":"Tight Bounds on the Complexity of Cascaded Decomposition of Automata. In 31st Annual Symposium on Foundations of Computer Science, St","author":"Maler Oded","year":"1990","unstructured":"Oded Maler and Amir Pnueli . 1990 . Tight Bounds on the Complexity of Cascaded Decomposition of Automata. In 31st Annual Symposium on Foundations of Computer Science, St . Louis, Missouri, USA , October 22-24, 1990, Volume II . IEEE Computer Society, 672--682. https:\/\/doi.org\/10.1109\/FSCS.1990.89589 10.1109\/FSCS.1990.89589 Oded Maler and Amir Pnueli. 1990. Tight Bounds on the Complexity of Cascaded Decomposition of Automata. In 31st Annual Symposium on Foundations of Computer Science, St. Louis, Missouri, USA, October 22-24, 1990, Volume II. IEEE Computer Society, 672--682. https:\/\/doi.org\/10.1109\/FSCS.1990.89589"},{"key":"e_1_3_2_1_11_1","volume-title":"Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing, Quebec City","author":"Manna Zohar","year":"1990","unstructured":"Zohar Manna and Amir Pnueli . 1990 . A Hierarchy of Temporal Properties . In Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing, Quebec City , Quebec, Canada , August 22-24, 1990, Cynthia Dwork (Ed.). ACM, 377--410. 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 Ninth Annual ACM Symposium on Principles of Distributed Computing, Quebec City, Quebec, Canada, August 22-24, 1990, Cynthia Dwork (Ed.). ACM, 377--410. https:\/\/doi.org\/10.1145\/93385.93442"},{"key":"e_1_3_2_1_12_1","volume-title":"The temporal logic of reactive and concurrent systems - specification","author":"Manna Zohar","unstructured":"Zohar Manna and Amir Pnueli . 1992. The temporal logic of reactive and concurrent systems - specification . Springer . Zohar Manna and Amir Pnueli. 1992. The temporal logic of reactive and concurrent systems - specification. Springer."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90049-5"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5139"},{"key":"e_1_3_2_1_15_1","volume-title":"Lecture Notes in Computer Science","author":"Nipkow Tobias","unstructured":"Tobias Nipkow , Lawrence C. Paulson , and Markus Wenzel . 2002. Isabelle\/ HOL - A Proof Assistant for Higher-Order Logic . Lecture Notes in Computer Science , Vol. 2283 . Springer . https:\/\/doi.org\/10.1007\/3-540-45949-9 10.1007\/3-540-45949-9 Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283. Springer. https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"e_1_3_2_1_16_1","volume-title":"10th International Conference, CIAA 2005","volume":"249","author":"Pel\u00e1nek Radek","year":"2005","unstructured":"Radek Pel\u00e1nek and Jan Strejcek . 2005 . Deeper Connections Between LTL and Alternating Automata. In Implementation and Application of Automata , 10th International Conference, CIAA 2005 , Sophia Antipolis, France , June 27-29, 2005, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 3845), Jacques Farr\u00e9, Igor Litovsky, and Sylvain Schmitz (Eds.). Springer, 238-- 249 . https:\/\/doi.org\/10.1007\/11605157_20 10.1007\/11605157_20 Radek Pel\u00e1nek and Jan Strejcek. 2005. Deeper Connections Between LTL and Alternating Automata. In Implementation and Application of Automata, 10th International Conference, CIAA 2005, Sophia Antipolis, France, June 27-29, 2005, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 3845), Jacques Farr\u00e9, Igor Litovsky, and Sylvain Schmitz (Eds.). Springer, 238--249. https:\/\/doi.org\/10.1007\/11605157_20"},{"key":"e_1_3_2_1_17_1","volume-title":"Handbook of Model Checking, Edmund M","author":"Piterman Nir","unstructured":"Nir Piterman and Amir Pnueli . 2018. Temporal Logic and Fair Discrete Systems . In Handbook of Model Checking, Edmund M . Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (Eds.). Springer , 27--73. https:\/\/doi.org\/10.1007\/978-3-319-10575--8_2 10.1007\/978-3-319-10575--8_2 Nir Piterman and Amir Pnueli. 2018. Temporal Logic and Fair Discrete Systems. In Handbook of Model Checking, Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (Eds.). Springer, 27--73. https:\/\/doi.org\/10.1007\/978-3-319-10575--8_2"},{"key":"e_1_3_2_1_18_1","volume-title":"Verification of Reactive Systems - Formal Methods and Algorithms","author":"Schneider Klaus","unstructured":"Klaus Schneider . 2004. Verification of Reactive Systems - Formal Methods and Algorithms . Springer . https:\/\/doi.org\/10.1007\/978-3-662-10778-2 10.1007\/978-3-662-10778-2 Klaus Schneider. 2004. Verification of Reactive Systems - Formal Methods and Algorithms. Springer. https:\/\/doi.org\/10.1007\/978-3-662-10778-2"},{"key":"e_1_3_2_1_19_1","volume-title":"A Compositional and Unified Translation of LTL into \u03c9-Automata. Archive of Formal Proofs 2019","author":"Seidl Benedikt","year":"2019","unstructured":"Benedikt Seidl and Salomon Sickert . 2019. A Compositional and Unified Translation of LTL into \u03c9-Automata. Archive of Formal Proofs 2019 ( 2019 ). https:\/\/www.isa-afp.org\/entries\/LTL_Master_Theorem.html Benedikt Seidl and Salomon Sickert. 2019. A Compositional and Unified Translation of LTL into \u03c9-Automata. Archive of Formal Proofs 2019 (2019). https:\/\/www.isa-afp.org\/entries\/LTL_Master_Theorem.html"},{"key":"e_1_3_2_1_20_1","volume-title":"Linear Temporal Logic. Archive of Formal Proofs 2016","author":"Sickert Salomon","year":"2016","unstructured":"Salomon Sickert . 2016. Linear Temporal Logic. Archive of Formal Proofs 2016 ( 2016 ). https:\/\/www.isa-afp.org\/entries\/LTL.shtml Salomon Sickert. 2016. Linear Temporal Logic. Archive of Formal Proofs 2016 (2016). https:\/\/www.isa-afp.org\/entries\/LTL.shtml"},{"key":"e_1_3_2_1_22_1","volume-title":"An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle\/HOL Formalisation. Archive of Formal Proofs 2020","author":"Sickert Salomon","year":"2020","unstructured":"Salomon Sickert . 2020. An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle\/HOL Formalisation. Archive of Formal Proofs 2020 ( 2020 ). https:\/\/www.isa-afp.org\/entries\/LTL_Normal_Form.html Salomon Sickert. 2020. An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle\/HOL Formalisation. Archive of Formal Proofs 2020 (2020). https:\/\/www.isa-afp.org\/entries\/LTL_Normal_Form.html"},{"key":"e_1_3_2_1_23_1","volume-title":"An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata. CoRR abs\/2005.00472","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. CoRR abs\/2005.00472 ( 2020 ). http:\/\/arxiv.org\/abs\/2005.00472 Salomon Sickert and Javier Esparza. 2020. An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata. CoRR abs\/2005.00472 (2020). http:\/\/arxiv.org\/abs\/2005.00472"},{"key":"e_1_3_2_1_24_1","volume-title":"International Conference TACS '94, Sendai, Japan, April 19-22, 1994, Proceedings (Lecture Notes in Computer Science","volume":"597","author":"Vardi Moshe Y.","year":"1994","unstructured":"Moshe Y. Vardi . 1994 . Nontraditional Applications of Automata Theory. In Theoretical Aspects of Computer Software , International Conference TACS '94, Sendai, Japan, April 19-22, 1994, Proceedings (Lecture Notes in Computer Science , Vol. 789), Masami Hagiya and John C. Mitchell (Eds.). Springer, 575-- 597 . https:\/\/doi.org\/10.1007\/3-540-57887-0_116 10.1007\/3-540-57887-0_116 Moshe Y. Vardi. 1994. Nontraditional Applications of Automata Theory. In Theoretical Aspects of Computer Software, International Conference TACS '94, Sendai, Japan, April 19-22, 1994, Proceedings (Lecture Notes in Computer Science, Vol. 789), Masami Hagiya and John C. Mitchell (Eds.). Springer, 575--597. https:\/\/doi.org\/10.1007\/3-540-57887-0_116"}],"event":{"name":"LICS '20: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Saarbr\u00fccken Germany","acronym":"LICS '20","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"]},"container-title":["Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394743","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394743","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:35Z","timestamp":1750197755000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394743"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,8]]},"references-count":23,"alternative-id":["10.1145\/3373718.3394743","10.1145\/3373718"],"URL":"https:\/\/doi.org\/10.1145\/3373718.3394743","relation":{},"subject":[],"published":{"date-parts":[[2020,7,8]]},"assertion":[{"value":"2020-07-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}