{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T11:04:48Z","timestamp":1768907088819,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,8,2]],"date-time":"2022-08-02T00:00:00Z","timestamp":1659398400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Deutsche Forschungsgemeinschaft (DFG)","award":["389792660, TRR 248"],"award-info":[{"award-number":["389792660, TRR 248"]}]},{"name":"Bundesministerium f\u00fcr Bildung und Forschung (BMBF)","award":["ScaDS.AI"],"award-info":[{"award-number":["ScaDS.AI"]}]},{"name":"Center for Advancing Electronics Dresden"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,8,2]]},"DOI":"10.1145\/3531130.3533369","type":"proceedings-article","created":{"date-parts":[[2022,8,4]],"date-time":"2022-08-04T20:23:38Z","timestamp":1659644618000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Deciding Hyperproperties Combined with Functional Specifications"],"prefix":"10.1145","author":[{"given":"Raven","family":"Beutner","sequence":"first","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Germany"}]},{"given":"David","family":"Carral","sequence":"additional","affiliation":[{"name":"Sophia Antipolis - M\u00e9diterran\u00e9e Centre, Inria, France and Laboratoire d\u2019Informatique, de Robotique et de Micro\u00e9lectronique de Montpellier (LIRMM), University of Montpellier, France"}]},{"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Germany"}]},{"given":"Jana","family":"Hofmann","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Germany"}]},{"given":"Markus","family":"Kr\u00f6tzsch","sequence":"additional","affiliation":[{"name":"TU Dresden, Germany"}]}],"member":"320","published-online":{"date-parts":[[2022,8,4]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Probabilistic Hyperproperties with Nondeterminism. In International Symposium on Automated Technology for Verification and Analysis, ATVA 2020(Lecture Notes in Computer Science, Vol.\u00a012302)","author":"\u00c1brah\u00e1m Erika","year":"2020","unstructured":"Erika \u00c1brah\u00e1m , Ezio Bartocci , Borzoo Bonakdarpour , and Oyendrila Dobe . 2020 . Probabilistic Hyperproperties with Nondeterminism. In International Symposium on Automated Technology for Verification and Analysis, ATVA 2020(Lecture Notes in Computer Science, Vol.\u00a012302) . Springer. https:\/\/doi.org\/10.1007\/978-3-030-59152-6_29 10.1007\/978-3-030-59152-6_29 Erika \u00c1brah\u00e1m, Ezio Bartocci, Borzoo Bonakdarpour, and Oyendrila Dobe. 2020. Probabilistic Hyperproperties with Nondeterminism. In International Symposium on Automated Technology for Verification and Analysis, ATVA 2020(Lecture Notes in Computer Science, Vol.\u00a012302). Springer. https:\/\/doi.org\/10.1007\/978-3-030-59152-6_29"},{"key":"e_1_3_2_1_2_1","article-title":"Defining","volume":"21","author":"Alpern Bowen","year":"1985","unstructured":"Bowen Alpern and Fred\u00a0 B. Schneider . 1985 . Defining Liveness. Inf. Process. Lett. 21 , 4 (1985). https:\/\/doi.org\/10.1016\/0020-0190(85)90056-0 10.1016\/0020-0190(85)90056-0 Bowen Alpern and Fred\u00a0B. Schneider. 1985. Defining Liveness. Inf. Process. Lett. 21, 4 (1985). https:\/\/doi.org\/10.1016\/0020-0190(85)90056-0","journal-title":"Liveness. Inf. Process. Lett."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/174644.174651"},{"key":"e_1_3_2_1_4_1","volume-title":"Flavors of Sequential Information Flow. In International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2022(Lecture Notes in Computer Science, Vol.\u00a013182)","author":"Bartocci Ezio","year":"2022","unstructured":"Ezio Bartocci , Thomas Ferr\u00e8re , Thomas\u00a0 A. Henzinger , Dejan Nickovic , and Ana\u00a0Oliveira da Costa . 2022 . Flavors of Sequential Information Flow. In International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2022(Lecture Notes in Computer Science, Vol.\u00a013182) . Springer. https:\/\/doi.org\/10.1007\/978-3-030-94583-1_1 10.1007\/978-3-030-94583-1_1 Ezio Bartocci, Thomas Ferr\u00e8re, Thomas\u00a0A. Henzinger, Dejan Nickovic, and Ana\u00a0Oliveira da Costa. 2022. Flavors of Sequential Information Flow. In International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2022(Lecture Notes in Computer Science, Vol.\u00a013182). Springer. https:\/\/doi.org\/10.1007\/978-3-030-94583-1_1"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_33"},{"key":"e_1_3_2_1_6_1","unstructured":"Raven Beutner David Carral Bernd Finkbeiner Jana Hofmann and Markus Kr\u00f6tzsch. 2022. Deciding Hyperproperties Combined with Functional Specifications. CoRR abs\/2205.15138(2022). arXiv:2205.15138  Raven Beutner David Carral Bernd Finkbeiner Jana Hofmann and Markus Kr\u00f6tzsch. 2022. Deciding Hyperproperties Combined with Functional Specifications. CoRR abs\/2205.15138(2022). arXiv:2205.15138"},{"key":"e_1_3_2_1_7_1","volume-title":"International Conference on Concurrency Theory, CONCUR 2021(LIPIcs, Vol.\u00a0203)","author":"Beutner Raven","year":"2021","unstructured":"Raven Beutner and Bernd Finkbeiner . 2021 . A Temporal Logic for Strategic Hyperproperties . In International Conference on Concurrency Theory, CONCUR 2021(LIPIcs, Vol.\u00a0203) . Schloss Dagstuhl. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR. 2021.24 10.4230\/LIPIcs.CONCUR.2021.24 Raven Beutner and Bernd Finkbeiner. 2021. A Temporal Logic for Strategic Hyperproperties. In International Conference on Concurrency Theory, CONCUR 2021(LIPIcs, Vol.\u00a0203). Schloss Dagstuhl. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2021.24"},{"key":"e_1_3_2_1_8_1","volume-title":"Prophecy Variables for Hyperproperty Verification. In IEEE Computer Security Foundations Symposium, CSF","author":"Beutner Raven","year":"2022","unstructured":"Raven Beutner and Bernd Finkbeiner . 2022 . Prophecy Variables for Hyperproperty Verification. In IEEE Computer Security Foundations Symposium, CSF 2022. IEEE. Raven Beutner and Bernd Finkbeiner. 2022. Prophecy Variables for Hyperproperty Verification. In IEEE Computer Security Foundations Symposium, CSF 2022. IEEE."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_17"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Borzoo Bonakdarpour and Sarai Sheinvald. 2022. Finite-Word Hyperlanguages. arxiv:2201.01670  Borzoo Bonakdarpour and Sarai Sheinvald. 2022. Finite-Word Hyperlanguages. arxiv:2201.01670","DOI":"10.1016\/j.ic.2022.104944"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63141-0_10"},{"key":"e_1_3_2_1_12_1","volume-title":"Asynchronous Extensions of HyperLTL. In Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021","author":"Bozzelli Laura","year":"2021","unstructured":"Laura Bozzelli , Adriano Peron , and C\u00e9sar S\u00e1nchez . 2021 . Asynchronous Extensions of HyperLTL. In Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021 . IEEE. https:\/\/doi.org\/10.1109\/LICS52264.2021.9470583 10.1109\/LICS52264.2021.9470583 Laura Bozzelli, Adriano Peron, and C\u00e9sar S\u00e1nchez. 2021. Asynchronous Extensions of HyperLTL. In Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021. IEEE. https:\/\/doi.org\/10.1109\/LICS52264.2021.9470583"},{"key":"e_1_3_2_1_13_1","volume-title":"Temporal Logics for Hyperproperties. In International Conference on Principles of Security and Trust, POST 2014(Lecture Notes in Computer Science, Vol.\u00a08414)","author":"Clarkson R.","year":"2014","unstructured":"Michael\u00a0 R. Clarkson , Bernd Finkbeiner , Masoud Koleini , Kristopher\u00a0 K. Micinski , Markus\u00a0 N. Rabe , and C\u00e9sar S\u00e1nchez . 2014 . Temporal Logics for Hyperproperties. In International Conference on Principles of Security and Trust, POST 2014(Lecture Notes in Computer Science, Vol.\u00a08414) . Springer. https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15 10.1007\/978-3-642-54792-8_15 Michael\u00a0R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher\u00a0K. Micinski, Markus\u00a0N. Rabe, and C\u00e9sar S\u00e1nchez. 2014. Temporal Logics for Hyperproperties. In International Conference on Principles of Security and Trust, POST 2014(Lecture Notes in Computer Science, Vol.\u00a08414). Springer. https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15"},{"key":"e_1_3_2_1_14_1","volume-title":"Hyperproperties. In IEEE Computer Security Foundations Symposium, CSF 2008","author":"R.","year":"2008","unstructured":"Michael\u00a0 R. Clarkson and Fred\u00a0B. Schneider. 2008 . Hyperproperties. In IEEE Computer Security Foundations Symposium, CSF 2008 . IEEE. https:\/\/doi.org\/10.1109\/CSF. 2008 .7 10.1109\/CSF.2008.7 Michael\u00a0R. Clarkson and Fred\u00a0B. Schneider. 2008. Hyperproperties. In IEEE Computer Security Foundations Symposium, CSF 2008. IEEE. https:\/\/doi.org\/10.1109\/CSF.2008.7"},{"key":"e_1_3_2_1_15_1","volume-title":"The Hierarchy of Hyperlogics. In Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2019","author":"Coenen Norine","year":"2019","unstructured":"Norine Coenen , Bernd Finkbeiner , Christopher Hahn , and Jana Hofmann . 2019 . The Hierarchy of Hyperlogics. In Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2019 . IEEE. https:\/\/doi.org\/10.1109\/LICS.2019.8785713 10.1109\/LICS.2019.8785713 Norine Coenen, Bernd Finkbeiner, Christopher Hahn, and Jana Hofmann. 2019. The Hierarchy of Hyperlogics. In Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2019. IEEE. https:\/\/doi.org\/10.1109\/LICS.2019.8785713"},{"key":"e_1_3_2_1_16_1","volume-title":"Programs. In European Symposium on Programming, ESOP 2017(Lecture Notes in Computer Science, Vol.\u00a010201)","author":"D\u2019Argenio R.","year":"2017","unstructured":"Pedro\u00a0 R. D\u2019Argenio , Gilles Barthe , Sebastian Biewer , Bernd Finkbeiner , and Holger Hermanns . 2017 . Is Your Software on Dope? - Formal Analysis of Surreptitiously \u201denhanced \u201d Programs. In European Symposium on Programming, ESOP 2017(Lecture Notes in Computer Science, Vol.\u00a010201) . Springer. https:\/\/doi.org\/10.1007\/978-3-662-54434-1_4 10.1007\/978-3-662-54434-1_4 Pedro\u00a0R. D\u2019Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, and Holger Hermanns. 2017. Is Your Software on Dope? - Formal Analysis of Surreptitiously \u201denhanced\u201d Programs. In European Symposium on Programming, ESOP 2017(Lecture Notes in Computer Science, Vol.\u00a010201). Springer. https:\/\/doi.org\/10.1007\/978-3-662-54434-1_4"},{"key":"e_1_3_2_1_17_1","volume-title":"Probabilistic Hyperproperties of Markov Decision Processes. In International Symposium on Automated Technology for Verification and Analysis, ATVA 2020(Lecture Notes in Computer Science, Vol.\u00a012302)","author":"Dimitrova Rayna","year":"2020","unstructured":"Rayna Dimitrova , Bernd Finkbeiner , and Hazem Torfah . 2020 . Probabilistic Hyperproperties of Markov Decision Processes. In International Symposium on Automated Technology for Verification and Analysis, ATVA 2020(Lecture Notes in Computer Science, Vol.\u00a012302) . Springer. https:\/\/doi.org\/10.1007\/978-3-030-59152-6_27 10.1007\/978-3-030-59152-6_27 Rayna Dimitrova, Bernd Finkbeiner, and Hazem Torfah. 2020. Probabilistic Hyperproperties of Markov Decision Processes. In International Symposium on Automated Technology for Verification and Analysis, ATVA 2020(Lecture Notes in Computer Science, Vol.\u00a012302). Springer. https:\/\/doi.org\/10.1007\/978-3-030-59152-6_27"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00009"},{"key":"e_1_3_2_1_20_1","volume-title":"Deciding Hyperproperties. In International Conference on Concurrency Theory, CONCUR 2016(LIPIcs, Vol.\u00a059)","author":"Finkbeiner Bernd","year":"2016","unstructured":"Bernd Finkbeiner and Christopher Hahn . 2016 . Deciding Hyperproperties. In International Conference on Concurrency Theory, CONCUR 2016(LIPIcs, Vol.\u00a059) . Schloss Dagstuhl. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR. 2016.13 10.4230\/LIPIcs.CONCUR.2016.13 Bernd Finkbeiner and Christopher Hahn. 2016. Deciding Hyperproperties. In International Conference on Concurrency Theory, CONCUR 2016(LIPIcs, Vol.\u00a059). Schloss Dagstuhl. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.13"},{"key":"e_1_3_2_1_21_1","volume-title":"International Symposium on Automated Technology for Verification and Analysis, ATVA 2018(Lecture Notes in Computer Science, Vol.\u00a011138)","author":"Finkbeiner Bernd","year":"2018","unstructured":"Bernd Finkbeiner , Christopher Hahn , and Tobias Hans . 2018 . MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the \u2203*\u2200* Fragment . In International Symposium on Automated Technology for Verification and Analysis, ATVA 2018(Lecture Notes in Computer Science, Vol.\u00a011138) . Springer. https:\/\/doi.org\/10.1007\/978-3-030-01090-4_31 10.1007\/978-3-030-01090-4_31 Bernd Finkbeiner, Christopher Hahn, and Tobias Hans. 2018. MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the \u2203*\u2200* Fragment. In International Symposium on Automated Technology for Verification and Analysis, ATVA 2018(Lecture Notes in Computer Science, Vol.\u00a011138). Springer. https:\/\/doi.org\/10.1007\/978-3-030-01090-4_31"},{"key":"e_1_3_2_1_22_1","volume-title":"Model Checking Quantitative Hyperproperties. In International Conference on Computer Aided Verification, CAV 2018(Lecture Notes in Computer Science, Vol.\u00a010981)","author":"Finkbeiner Bernd","year":"2018","unstructured":"Bernd Finkbeiner , Christopher Hahn , and Hazem Torfah . 2018 . Model Checking Quantitative Hyperproperties. In International Conference on Computer Aided Verification, CAV 2018(Lecture Notes in Computer Science, Vol.\u00a010981) . Springer. https:\/\/doi.org\/10.1007\/978-3-319-96145-3_8 10.1007\/978-3-319-96145-3_8 Bernd Finkbeiner, Christopher Hahn, and Hazem Torfah. 2018. Model Checking Quantitative Hyperproperties. In International Conference on Computer Aided Verification, CAV 2018(Lecture Notes in Computer Science, Vol.\u00a010981). Springer. https:\/\/doi.org\/10.1007\/978-3-319-96145-3_8"},{"key":"e_1_3_2_1_23_1","volume-title":"The First-Order Logic of Hyperproperties. In Symposium on Theoretical Aspects of Computer Science, STACS 2017(LIPIcs, Vol.\u00a066)","author":"Finkbeiner Bernd","year":"2017","unstructured":"Bernd Finkbeiner and Martin Zimmermann . 2017 . The First-Order Logic of Hyperproperties. In Symposium on Theoretical Aspects of Computer Science, STACS 2017(LIPIcs, Vol.\u00a066) . Schloss Dagstuhl. https:\/\/doi.org\/10.4230\/LIPIcs.STACS. 2017.30 10.4230\/LIPIcs.STACS.2017.30 Bernd Finkbeiner and Martin Zimmermann. 2017. The First-Order Logic of Hyperproperties. In Symposium on Theoretical Aspects of Computer Science, STACS 2017(LIPIcs, Vol.\u00a066). Schloss Dagstuhl. https:\/\/doi.org\/10.4230\/LIPIcs.STACS.2017.30"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"e_1_3_2_1_25_1","volume-title":"International Symposium on Mathematical Foundations of Computer Science, MFCS 2021(LIPIcs, Vol.\u00a0202)","author":"Fortin Marie","year":"2021","unstructured":"Marie Fortin , Louwe\u00a0 B. Kuijer , Patrick Totzke , and Martin Zimmermann . 2021 . HyperLTL Satisfiability is -complete, HyperCTL* Satisfiability is -complete . In International Symposium on Mathematical Foundations of Computer Science, MFCS 2021(LIPIcs, Vol.\u00a0202) . Schloss Dagstuhl. https:\/\/doi.org\/10.4230\/LIPIcs.MFCS. 2021.47 10.4230\/LIPIcs.MFCS.2021.47 Marie Fortin, Louwe\u00a0B. Kuijer, Patrick Totzke, and Martin Zimmermann. 2021. HyperLTL Satisfiability is -complete, HyperCTL* Satisfiability is -complete. In International Symposium on Mathematical Foundations of Computer Science, MFCS 2021(LIPIcs, Vol.\u00a0202). Schloss Dagstuhl. https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2021.47"},{"key":"e_1_3_2_1_26_1","unstructured":"Kurt G\u00f6del. 1929. \u00dcber die vollst\u00e4ndigkeit des logikkalk\u00fcls.  Kurt G\u00f6del. 1929. \u00dcber die vollst\u00e4ndigkeit des logikkalk\u00fcls."},{"key":"e_1_3_2_1_27_1","volume-title":"Propositional Dynamic Logic for Hyperproperties. In International Conference on Concurrency Theory, CONCUR 2020(LIPIcs, Vol.\u00a0171)","author":"Gutsfeld Jens\u00a0Oliver","year":"2020","unstructured":"Jens\u00a0Oliver Gutsfeld , Markus M\u00fcller-Olm , and Christoph Ohrem . 2020 . Propositional Dynamic Logic for Hyperproperties. In International Conference on Concurrency Theory, CONCUR 2020(LIPIcs, Vol.\u00a0171) . Schloss Dagstuhl. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR. 2020.50 10.4230\/LIPIcs.CONCUR.2020.50 Jens\u00a0Oliver Gutsfeld, Markus M\u00fcller-Olm, and Christoph Ohrem. 2020. Propositional Dynamic Logic for Hyperproperties. In International Conference on Concurrency Theory, CONCUR 2020(LIPIcs, Vol.\u00a0171). Schloss Dagstuhl. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.50"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434319"},{"key":"e_1_3_2_1_29_1","volume-title":"Reachability in Succinct and Parametric One-Counter Automata. In International Conference on Concurrency Theory, CONCUR 2009(Lecture Notes in Computer Science, Vol.\u00a05710)","author":"Haase Christoph","year":"2009","unstructured":"Christoph Haase , Stephan Kreutzer , Jo\u00ebl Ouaknine , and James Worrell . 2009 . Reachability in Succinct and Parametric One-Counter Automata. In International Conference on Concurrency Theory, CONCUR 2009(Lecture Notes in Computer Science, Vol.\u00a05710) . Springer. https:\/\/doi.org\/10.1007\/978-3-642-04081-8_25 10.1007\/978-3-642-04081-8_25 Christoph Haase, Stephan Kreutzer, Jo\u00ebl Ouaknine, and James Worrell. 2009. Reachability in Succinct and Parametric One-Counter Automata. In International Conference on Concurrency Theory, CONCUR 2009(Lecture Notes in Computer Science, Vol.\u00a05710). Springer. https:\/\/doi.org\/10.1007\/978-3-642-04081-8_25"},{"key":"e_1_3_2_1_30_1","volume-title":"Team Semantics for the Specification and Verification of Hyperproperties. In International Symposium on Mathematical Foundations of Computer Science, MFCS 2018(LIPIcs, Vol.\u00a0117)","author":"Krebs Andreas","year":"2018","unstructured":"Andreas Krebs , Arne Meier , Jonni Virtema , and Martin Zimmermann . 2018 . Team Semantics for the Specification and Verification of Hyperproperties. In International Symposium on Mathematical Foundations of Computer Science, MFCS 2018(LIPIcs, Vol.\u00a0117) . Schloss Dagstuhl. https:\/\/doi.org\/10.4230\/LIPIcs.MFCS. 2018.10 10.4230\/LIPIcs.MFCS.2018.10 Andreas Krebs, Arne Meier, Jonni Virtema, and Martin Zimmermann. 2018. Team Semantics for the Specification and Verification of Hyperproperties. In International Symposium on Mathematical Foundations of Computer Science, MFCS 2018(LIPIcs, Vol.\u00a0117). Schloss Dagstuhl. https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2018.10"},{"key":"e_1_3_2_1_31_1","volume-title":"Model Checking of Safety Properties. In International Conference on Computer Aided Verification, CAV 1999(Lecture Notes in Computer Science, Vol.\u00a01633)","author":"Kupferman Orna","year":"1999","unstructured":"Orna Kupferman and Moshe\u00a0 Y. Vardi . 1999 . Model Checking of Safety Properties. In International Conference on Computer Aided Verification, CAV 1999(Lecture Notes in Computer Science, Vol.\u00a01633) . Springer. https:\/\/doi.org\/10.1007\/3-540-48683-6_17 10.1007\/3-540-48683-6_17 Orna Kupferman and Moshe\u00a0Y. Vardi. 1999. Model Checking of Safety Properties. In International Conference on Computer Aided Verification, CAV 1999(Lecture Notes in Computer Science, Vol.\u00a01633). Springer. https:\/\/doi.org\/10.1007\/3-540-48683-6_17"},{"key":"e_1_3_2_1_32_1","unstructured":"Martin L\u00fcck. 2016. Complete Problems of Propositional Logic for the Exponential Hierarchy. CoRR abs\/1602.03050(2016). arXiv:1602.03050  Martin L\u00fcck. 2016. Complete Problems of Propositional Logic for the Exponential Hierarchy. CoRR abs\/1602.03050(2016). arXiv:1602.03050"},{"key":"e_1_3_2_1_33_1","volume-title":"EACSL Annual Conference on Computer Science Logic, CSL 2020(LIPIcs, Vol.\u00a0152)","author":"Mascle Corto","year":"2020","unstructured":"Corto Mascle and Martin Zimmermann . 2020 . The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas . In EACSL Annual Conference on Computer Science Logic, CSL 2020(LIPIcs, Vol.\u00a0152) . Schloss Dagstuhl. https:\/\/doi.org\/10.4230\/LIPIcs.CSL. 2020.29 10.4230\/LIPIcs.CSL.2020.29 Corto Mascle and Martin Zimmermann. 2020. The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas. In EACSL Annual Conference on Computer Science Logic, CSL 2020(LIPIcs, Vol.\u00a0152). Schloss Dagstuhl. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2020.29"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1988.8110"},{"key":"e_1_3_2_1_35_1","volume-title":"Computation","author":"Minsky Marvin\u00a0Lee","unstructured":"Marvin\u00a0Lee Minsky . 1967. Computation . Prentice-Hall Englewood Cliffs . Marvin\u00a0Lee Minsky. 1967. Computation. Prentice-Hall Englewood Cliffs."},{"key":"e_1_3_2_1_37_1","unstructured":"John\u00a0Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning. MIT Press.  John\u00a0Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning. MIT Press."},{"key":"e_1_3_2_1_38_1","volume-title":"Theory of recursive functions and effective computability","author":"Rogers\u00a0Jr Hartley","unstructured":"Hartley Rogers\u00a0Jr . 1987. Theory of recursive functions and effective computability . MIT press . Hartley Rogers\u00a0Jr. 1987. Theory of recursive functions and effective computability. MIT press."},{"key":"e_1_3_2_1_39_1","volume-title":"liveness and fairness in temporal logic. Formal Aspects of Computing 6, 5","author":"Sistla A\u00a0Prasad","year":"1994","unstructured":"A\u00a0Prasad Sistla . 1994. Safety , liveness and fairness in temporal logic. Formal Aspects of Computing 6, 5 ( 1994 ). A\u00a0Prasad Sistla. 1994. Safety, liveness and fairness in temporal logic. Formal Aspects of Computing 6, 5 (1994)."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"e_1_3_2_1_41_1","volume-title":"The Polynomial-Time Hierarchy. Theor. Comput. Sci. 3, 1","author":"Stockmeyer J.","year":"1976","unstructured":"Larry\u00a0 J. Stockmeyer . 1976. The Polynomial-Time Hierarchy. Theor. Comput. Sci. 3, 1 ( 1976 ). https:\/\/doi.org\/10.1016\/0304-3975(76)90061-X 10.1016\/0304-3975(76)90061-X Larry\u00a0J. Stockmeyer. 1976. The Polynomial-Time Hierarchy. Theor. Comput. Sci. 3, 1 (1976). https:\/\/doi.org\/10.1016\/0304-3975(76)90061-X"},{"key":"e_1_3_2_1_42_1","volume-title":"Vardi and Pierre Wolper","author":"Y.","year":"1994","unstructured":"Moshe\u00a0 Y. Vardi and Pierre Wolper . 1994 . Reasoning About Infinite Computations. Inf. Comput . 115, 1 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1092 10.1006\/inco.1994.1092 Moshe\u00a0Y. Vardi and Pierre Wolper. 1994. Reasoning About Infinite Computations. Inf. Comput. 115, 1 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1092"},{"key":"#cr-split#-e_1_3_2_1_43_1.1","unstructured":"Jonni Virtema Jana Hofmann Bernd Finkbeiner Juha Kontinen and Fan Yang. 2021. Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science FSTTCS 2021(LIPIcs Vol.\u00a0213). Schloss Dagstuhl. https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2021.52 10.4230\/LIPIcs.FSTTCS.2021.52"},{"key":"#cr-split#-e_1_3_2_1_43_1.2","unstructured":"Jonni Virtema Jana Hofmann Bernd Finkbeiner Juha Kontinen and Fan Yang. 2021. Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science FSTTCS 2021(LIPIcs Vol.\u00a0213). Schloss Dagstuhl. https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2021.52"}],"event":{"name":"LICS '22: 37th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Haifa Israel","acronym":"LICS '22","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3531130.3533369","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3531130.3533369","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:10Z","timestamp":1750186930000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3531130.3533369"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,2]]},"references-count":43,"alternative-id":["10.1145\/3531130.3533369","10.1145\/3531130"],"URL":"https:\/\/doi.org\/10.1145\/3531130.3533369","relation":{},"subject":[],"published":{"date-parts":[[2022,8,2]]},"assertion":[{"value":"2022-08-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}