{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T11:19:00Z","timestamp":1782991140861,"version":"3.54.5"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227294","type":"print"},{"value":"9783032227300","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22730-0_14","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T16:24:38Z","timestamp":1776270278000},"page":"285-306","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Complexity of Model Checking Second-Order Hyperproperties on Finite Structures"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4280-8441","authenticated-orcid":false,"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3566-0338","authenticated-orcid":false,"given":"Hadar","family":"Frenkel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-2419-1604","authenticated-orcid":false,"given":"Tim","family":"Rohde","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,15]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Henzinger, T.A., Nickovic, D., da Costa, A.O.: Hypernode automata. In: P\u00e9rez, G.A., Raskin, J. (eds.) CONCUR 2023. LIPIcs, vol. 279, pp. 21:1\u201321:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2023.21","DOI":"10.4230\/LIPICS.CONCUR.2023.21"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Baumeister, J., Coenen, N., Bonakdarpour, B., Finkbeiner, B., S\u00e1nchez, C.: Atemporal logic for asynchronous hyperproperties. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021, Part I. LNCS, vol. 12759, pp. 694\u2013717. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_33","DOI":"10.1007\/978-3-030-81685-8_33"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: AutoHyper: Explicit-state model checking for HyperLTL. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023. vol. 13993. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_8","DOI":"10.1007\/978-3-031-30823-9_8"},{"key":"14_CR4","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B., Frenkel, H., Metzger, N.: Second-order hyperproperties. In: Enea, C., Lal, A. (eds.) CAV 2023, Part II. LNCS, vol. 13965, pp. 309\u2013332. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_15","DOI":"10.1007\/978-3-031-37703-7_15"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B., Frenkel, H., Metzger, N.: Monitoring second-order hyperproperties. In: Dastani, M., Sichman, J.S., Alechina, N., Dignum, V. (eds.) Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2024, Auckland, New Zealand, May 6-10, 2024. pp. 180\u2013188. International Foundation for Autonomous Agents and Multiagent Systems \/ ACM (2024). https:\/\/doi.org\/10.5555\/3635637.3662865, https:\/\/dl.acm.org\/doi\/10.5555\/3635637.3662865","DOI":"10.5555\/3635637.3662865"},{"key":"14_CR6","doi-asserted-by":"publisher","unstructured":"Bombardelli, A., Bozzelli, L., S\u00e1nchez, C., Tonetta, S.: Unifying asynchronous logics for hyperproperties. In: Barman, S., Lasota, S. (eds.) 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2024, December 16-18, 2024, Gandhinagar, Gujarat, India. LIPIcs,vol. 323, pp. 14:1\u201314:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPICS.FSTTCS.2024.14","DOI":"10.4230\/LIPICS.FSTTCS.2024.14"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Bonakdarpour, B., Finkbeiner, B.: The complexity of monitoring hyperproperties. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF). pp. 162\u2013174 (July 2018). https:\/\/doi.org\/10.1109\/CSF.2018.00019","DOI":"10.1109\/CSF.2018.00019"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Bozzelli, L., Maubert, B., Pinchinat, S.: Unifying hyper and epistemic temporallogics. In: Pitts, A.M. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 167\u2013182. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46678-0_11","DOI":"10.1007\/978-3-662-46678-0_11"},{"key":"14_CR9","doi-asserted-by":"publisher","unstructured":"Bozzelli, L., Peron, A., S\u00e1nchez, C.: Asynchronous extensions of HyperLTL. In: LICS 2021. pp. 1\u201313. IEEE (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470583","DOI":"10.1109\/LICS52264.2021.9470583"},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"Bozzelli, L., Peron, A., S\u00e1nchez, C.: Expressiveness and decidability of temporal logics for asynchronous hyperproperties. In: Klin, B., Lasota, S., Muscholl, A. (eds.) CONCUR 2022. LIPIcs, vol. 243, pp. 27:1\u201327:16. Schloss Dagstuhl - LeibnizZentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2022.27","DOI":"10.4230\/LIPIcs.CONCUR.2022.27"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265\u2013284. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"14_CR12","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010). https:\/\/doi.org\/10.3233\/JCS-2009-0393","DOI":"10.3233\/JCS-2009-0393"},{"key":"14_CR13","doi-asserted-by":"publisher","unstructured":"Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific (1995). https:\/\/doi.org\/10.1142\/2563","DOI":"10.1142\/2563"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt, W.A., Somenzi, F. (eds.) Computer Aided Verification. pp. 27\u201339. Springer Berlin Heidelberg, Berlin, Heidelberg (2003)","DOI":"10.1007\/978-3-540-45069-6_3"},{"key":"14_CR15","doi-asserted-by":"publisher","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press (1995). https:\/\/doi.org\/10.7551\/mitpress\/5803.001.0001","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Frenkel, H., Rohde, T.: Complexity of model checking second-order hyperproperties on finite structures (2026), https:\/\/arxiv.org\/abs\/2601.12361","DOI":"10.1007\/978-3-032-22730-0_14"},{"key":"14_CR17","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Efficient monitoring of hyperproperties using prefix trees. Int. J. Softw. Tools Technol. Transf. 22(6), 729\u2013740 (2020). https:\/\/doi.org\/10.1007\/S10009-020-00552-5","DOI":"10.1007\/S10009-020-00552-5"},{"key":"14_CR18","doi-asserted-by":"publisher","unstructured":"Fionda, V., Greco, G.: The complexity of LTL on finite traces: Hard and easy fragments. In: Schuurmans, D., Wellman, M.P. (eds.) Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, February 12-17, 2016, Phoenix, Arizona, USA. pp. 971\u2013977. AAAI Press (2016). https:\/\/doi.org\/10.1609\/AAAI.V30I1.10104","DOI":"10.1609\/AAAI.V30I1.10104"},{"key":"14_CR19","doi-asserted-by":"publisher","unstructured":"Fortin, M., Kuijer, L.B., Totzke, P., Zimmermann, M.: Hyperltl satisfiability is highly undecidable, hyperctl$$^*$$ is even harder. Log. Methods Comput. Sci. 21(1), 3 (2025). https:\/\/doi.org\/10.46298\/LMCS-21(1:3)2025","DOI":"10.46298\/LMCS-21(1:3)2025"},{"key":"14_CR20","doi-asserted-by":"publisher","unstructured":"Frenkel, H., Zimmermann, M.: The complexity of second-order hyperltl. In: Endrullis, J., Schmitz, S. (eds.) 33rd EACSL Annual Conference on Computer Science Logic, CSL 2025, February 10-14, 2025, Amsterdam, Netherlands. LIPIcs, vol. 326, pp. 10:1\u201310:23. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2025). https:\/\/doi.org\/10.4230\/LIPICS.CSL.2025.10","DOI":"10.4230\/LIPICS.CSL.2025.10"},{"key":"14_CR21","unstructured":"Garey, M.R., Johnson, D.S.: Computers and intractability. A series of books in the mathematical sciences, Freeman, New York, NY [u.a.] (1979), http:\/\/www.ulb.tu-darmstadt.de\/tocs\/5617215X.pdf"},{"key":"14_CR22","doi-asserted-by":"publisher","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, April 26-28, 1982. pp.11\u201320. IEEE Computer Society (1982). https:\/\/doi.org\/10.1109\/SP.1982.10014","DOI":"10.1109\/SP.1982.10014"},{"key":"14_CR23","doi-asserted-by":"publisher","unstructured":"Gutsfeld, J.O., M\u00fcller-Olm, M., Ohrem, C.: Automata and fixpoints for asynchronous hyperproperties. Proc. ACM Program. Lang. 5(POPL), 1\u201329 (2021). https:\/\/doi.org\/10.1145\/3434319","DOI":"10.1145\/3434319"},{"key":"14_CR24","doi-asserted-by":"publisher","unstructured":"Halpern, J.Y., Moses, Y.: Knowledge and common knowledge in a distributed environment. J. ACM 37(3), 549\u2013587 (1990). https:\/\/doi.org\/10.1145\/79147.79161","DOI":"10.1145\/79147.79161"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Hsu, T.H., Bonakdarpour, B., Finkbeiner, B., S\u00e1nchez, C.: Bounded model checking for asynchronous hyperproperties (2023)","DOI":"10.1007\/978-3-031-30823-9_2"},{"key":"14_CR26","doi-asserted-by":"publisher","unstructured":"Hsu, T., S\u00e1nchez, C., Bonakdarpour, B.: Bounded model checking for hyperproperties. In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12651, pp. 94\u2013112. Springer(2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_6","DOI":"10.1007\/978-3-030-72016-2_6"},{"key":"14_CR27","doi-asserted-by":"publisher","unstructured":"Kontinen, J., Sandstr\u00f6m, M., Virtema, J.: Set semantics for asynchronous TeamLTL: Expressivity and complexity. In: Leroux, J., Lombardy, S., Peleg, D. (eds.) MFCS 2023. LIPIcs, vol. 272, pp. 60:1\u201360:14. Schloss Dagstuhl - LeibnizZentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.MFCS.2023.60","DOI":"10.4230\/LIPICS.MFCS.2023.60"},{"key":"14_CR28","doi-asserted-by":"publisher","unstructured":"Kontinen, J., Sandstr\u00f6m, M., Virtema, J.: A remark on the expressivity of asynchronous TeamLTL and HyperLTL. In: Meier, A., Ortiz, M. (eds.) FoIKS 2024. LNCS, vol. 14589, pp. 275\u2013286. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-56940-1_15","DOI":"10.1007\/978-3-031-56940-1_15"},{"key":"14_CR29","doi-asserted-by":"publisher","unstructured":"Krebs, A., Meier, A., Virtema, J., Zimmermann, M.: Team semantics for the specification and verification of hyperproperties. In: Potapov, I., Spirakis, P.G., Worrell, J. (eds.) MFCS 2018. LIPIcs, vol. 117, pp. 10:1\u201310:16. Schloss Dagstuhl - LeibnizZentrum f\u00fcr Informatik (2018). https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2018.10","DOI":"10.4230\/LIPIcs.MFCS.2018.10"},{"key":"14_CR30","doi-asserted-by":"publisher","unstructured":"Kuhtz, L., Finkbeiner, B.: Weak kripke structures and LTL. In: Katoen, J., K\u00f6nig, B. (eds.) CONCUR 2011 - Concurrency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6901, pp. 419\u2013433. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-23217-6_28","DOI":"10.1007\/978-3-642-23217-6_28"},{"key":"14_CR31","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Halbwachs, N., Peled, D.A. (eds.) Computer Aided Verification, 11th International Conference, CAV \u201999, Trento, Italy, July 6-10, 1999, Proceedings. Lecture Notes in Computer Science, vol. 1633, pp. 172\u2013183. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_17","DOI":"10.1007\/3-540-48683-6_17"},{"key":"14_CR32","doi-asserted-by":"publisher","unstructured":"van der Meyden, R.: Common knowledge and update in finite environments. Inf. Comput. 140(2) (1998). https:\/\/doi.org\/10.1006\/inco.1997.2679","DOI":"10.1006\/inco.1997.2679"},{"key":"14_CR33","doi-asserted-by":"crossref","unstructured":"van der Meyden, R., Shilov, N.V.: Model checking knowledge and time in systems with perfect recall. In: FSTTCS. vol. 1738, pp. 432\u2013445. Springer (1999)","DOI":"10.1007\/3-540-46691-6_35"},{"key":"14_CR34","unstructured":"Papadimitriou, C.H.: Computational complexity. Theoretical computer science, Addison-Wesley, Reading, Massachusetts ([1994]), http:\/\/www.gbv.de\/dms\/ilmenau\/toc\/12708035X.PDF"},{"key":"14_CR35","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS 1977","DOI":"10.1109\/SFCS.1977.32"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22730-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T23:48:51Z","timestamp":1782949731000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22730-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227294","9783032227300"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22730-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"15 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2026\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}