{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,10]],"date-time":"2026-09-10T06:00:05Z","timestamp":1789020005470,"version":"build-2803163510"},"reference-count":74,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2023,4,1]],"date-time":"2023-04-01T00:00:00Z","timestamp":1680307200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM SIGLOG News"],"published-print":{"date-parts":[[2023,4]]},"abstract":"<jats:p>System requirements related to concepts like information flow, knowledge, and robustness cannot be judged in terms of individual system executions, but rather require an analysis of the relationship between multiple executions. Such requirements belong to the class of hyperproperties, which generalize classic trace properties to properties of sets of traces. During the past decade, a range of new specification logics has been introduced with the goal of providing a unified theory for reasoning about hyperproperties. This paper gives an overview on the current landscape of logics for the specification of hyperproperties and on algorithms for satisfiability checking, model checking, monitoring, and synthesis.<\/jats:p>","DOI":"10.1145\/3610392.3610394","type":"journal-article","created":{"date-parts":[[2023,7,19]],"date-time":"2023-07-19T20:22:19Z","timestamp":1689798139000},"page":"4-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Logics and Algorithms for Hyperproperties"],"prefix":"10.1145","volume":"10","author":[{"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[{"name":"CISPA Helmholtz Center for Information Security"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,7,19]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Automated Technology for Verification and Analysis","author":"\u00c1brah\u00e1m Erika","unstructured":"Erika \u00c1brah\u00e1m, Ezio Bartocci, Borzoo Bonakdarpour, and Oyendrila Dobe. 2020. Probabilistic Hyperproperties with Nondeterminism. In Automated Technology for Verification and Analysis, Dang Van Hung and Oleg Sokolsky (Eds.). Springer International Publishing, Cham, 518--534."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99154-2_2"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.24"},{"key":"e_1_2_1_5_1","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Discussion","author":"Barthe Gilles","unstructured":"Gilles Barthe, Pedro R. D'Argenio, Bernd Finkbeiner, and Holger Hermanns. 2016. Facets of Software Doping. In Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, Tiziana Margaria and Bernhard Steffen (Eds.). Springer International Publishing, Cham, 601--608."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000193"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158145"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2492061"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_33"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533369"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2021.24"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF54842.2022.9919658"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_17"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_8"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00019"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF49147.2020.00033"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_11"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470583"},{"key":"e_1_2_1_20_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Brett Noel","unstructured":"Noel Brett, Umair Siddique, and Borzoo Bonakdarpour. 2017. Rewriting-Based Runtime Verification for Alternation-Free HyperLTL. In Tools and Algorithms for the Construction and Analysis of Systems, Axel Legay and Tiziana Margaria (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 77--93."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2240236.2240262"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the 3rd Conference on Principles of Security and Trust (POST). 265--284","author":"Clarkson M. R.","unstructured":"M. R. Clarkson, B. Finkbeiner, M. Koleini, K. K. Micinski, M. N. Rabe, and C. S\u00e1nchez. 2014. Temporal Logics for Hyperproperties. In Proceedings of the 3rd Conference on Principles of Security and Trust (POST). 265--284."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.7"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 1st Workshop on Interactive Natural Language Technology for Explainable Artificial Intelligence. 8--13","author":"Miruna","year":"2019","unstructured":"Miruna A. Clinciu and Helen F. Hastie. 2019. A Survey of Explainable AI Terminology. In Proceedings of the 1st Workshop on Interactive Natural Language Technology for Explainable Artificial Intelligence. 8--13. 1st Workshop on Interactive Natural Language Technology for Explainable Artificial Intelligence, NL4XAI 2019."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785713"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF57540.2023.00006"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.15"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04761-9_24"},{"key":"e_1_2_1_30_1","volume-title":"Automated Technology for Verification and Analysis","author":"Dimitrova Rayna","unstructured":"Rayna Dimitrova, Bernd Finkbeiner, and Hazem Torfah. 2020. Probabilistic Hyperproperties of Markov Decision Processes. In Automated Technology for Verification and Analysis, Dang Van Hung and Oleg Sokolsky (Eds.). Springer International Publishing, Cham, 484--500."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","unstructured":"Geir Dullerud and Fernando Paganini. 2000. A Course in Robust Control Theory a convex approach. 10.1007\/978-1-4757-3290-0","DOI":"10.1007\/978-1-4757-3290-0"},{"key":"e_1_2_1_32_1","unstructured":"R. Fagin J. Y. Halpern Y. Moses and M. Y. Vardi. 2003. Reasoning about Knowledge. MIT Press Cambridge Mass."},{"key":"e_1_2_1_33_1","volume-title":"Bulletin of the EATCS 123","author":"Finkbeiner Bernd","year":"2017","unstructured":"Bernd Finkbeiner. 2017. Temporal Hyperproperties. Bulletin of the EATCS 123 (2017)."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_1"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2016.13"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_31"},{"key":"e_1_2_1_37_1","volume-title":"Computer Aided Verification","author":"Finkbeiner Bernd","unstructured":"Bernd Finkbeiner, Christopher Hahn, Jana Hofmann, and Leander Tentrup. 2020a. Realizing \u03c9-regular Hyperproperties. In Computer Aided Verification. Springer International Publishing, Cham, 40--63."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-019-00358-2"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_29"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_11"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-019-00334-z"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00552-5"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_35"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134080"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0228-z"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.STACS.2017.30"},{"key":"e_1_2_1_48_1","volume-title":"46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021","author":"Fortin Marie","year":"2021","unstructured":"Marie Fortin, Louwe B. Kuijer, Patrick Totzke, and Martin Zimmermann. 2021. HyperLTL Satisfiability is \u03a311-complete, HyperCTL* Satisfiability is \u03a321-complete. In 46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021, August 23--27, 2021, Tallinn, Estonia (LIPIcs), Filippo Bonchi and Simon J. Puglisi (Eds.), Vol. 202. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 47:1--47:19."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45656-2_15"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/567446.567462"},{"key":"e_1_2_1_51_1","volume-title":"Security Policies and Security Models. In IEEE Symposium on Security and Privacy. 11--20","author":"Joseph","unstructured":"Joseph A. Goguen and Jos\u00e9 Meseguer. 1982. Security Policies and Security Models. In IEEE Symposium on Security and Privacy. 11--20."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434319"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_7"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/79147.79161"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_2"},{"key":"e_1_2_1_56_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Hsu Tzu-Han","unstructured":"Tzu-Han Hsu, C\u00e9sar S\u00e1nchez, and Borzoo Bonakdarpour. 2021. Bounded Model Checking for Hyperproperties. In Tools and Algorithms for the Construction and Analysis of Systems, Jan Friso Groote and Kim Guldstrand Larsen (Eds.). Springer International Publishing, Cham, 94--112."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00766-008-0067-3"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1995.523239"},{"key":"e_1_2_1_60_1","volume-title":"2nd International Conference, ICTL '97, Manchester, England, July 14--18, 1997, Proceedings.","author":"Kupferman Orna","unstructured":"Orna Kupferman and Moshe Y. Vardi. 1997. Synthesis with incomplete information. In Temporal Logic, 2nd International Conference, ICTL '97, Manchester, England, July 14--18, 1997, Proceedings."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(4:17)2014"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_11"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2020.29"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1988.8110"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/RISP.1994.296590"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3457607"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127041.3127058"},{"key":"e_1_2_1_68_1","volume-title":"The Temporal Logic of Programs. In FOCS","author":"Pnueli Amir","year":"1977","unstructured":"Amir Pnueli. 1977. The Temporal Logic of Programs. In FOCS 1977. 46--57."},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1109\/FSCS.1990.89597"},{"key":"e_1_2_1_71_1","unstructured":"John Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning. Elsevier and MIT Press. https:\/\/www.sciencedirect.com\/book\/9780444508133\/handbook-of-automated-reasoning"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0352"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"e_1_2_1_75_1","volume-title":"Perspectives in Concurrency Theory, Kamal Lodaya, Madhavan Mukund, and R","author":"Thomas Wolfgang","unstructured":"Wolfgang Thomas. 2009. Path Logics with Synchronization. In Perspectives in Concurrency Theory, Kamal Lodaya, Madhavan Mukund, and R. Ramanujam (Eds.). IARCS-Universities, Universities Press, 469--481."},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00009"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/3358232"},{"key":"e_1_2_1_78_1","volume-title":"Proc. of CSFW'03","author":"Zdancewic S.","unstructured":"S. Zdancewic and A. C. Myers. 2003. Observational Determinism for Concurrent Program Security. In Proc. of CSFW'03."}],"container-title":["ACM SIGLOG News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3610392.3610394","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3610392.3610394","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:49:02Z","timestamp":1750182542000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3610392.3610394"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4]]},"references-count":74,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,4]]}},"alternative-id":["10.1145\/3610392.3610394"],"URL":"https:\/\/doi.org\/10.1145\/3610392.3610394","relation":{},"ISSN":["2372-3491"],"issn-type":[{"value":"2372-3491","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,4]]},"assertion":[{"value":"2023-07-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}