{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T06:47:39Z","timestamp":1767768459258,"version":"3.48.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032137104","type":"print"},{"value":"9783032137111","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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":7,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Hyperproperties are system properties that relate multiple traces (executions) of a system. Typical applications of hyperproperties are found in information flow security. In a previous paper, we introduced\n                    <jats:italic>concurrent<\/jats:italic>\n                    hyperproperties, by generalizing traces to\n                    <jats:italic>concurrent<\/jats:italic>\n                    traces, defined as partially ordered multisets. We take Petri nets as the basic semantic model. To check concurrent hyperproperties, we extended the testing of processes due to De Nicola and Hennessy to the setting of concurrent traces, using the parallel composition of Petri nets. In this paper, we present new results on decidability and undecidability of may and must testing of universal and existential concurrent hyperproperties, and analyze the case of concurrent hyperproperties with quantifier alternation.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-13711-1_9","type":"book-chapter","created":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T06:41:29Z","timestamp":1767768089000},"page":"135-153","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Concurrent $$\\forall \\exists $$-Hyperproperties"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4280-8441","authenticated-orcid":false,"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3600-2046","authenticated-orcid":false,"given":"Ernst-R\u00fcdiger","family":"Olderog","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-18419-8_9","volume-title":"Mathematical Models for the Semantics of Parallelism","author":"L Aceto","year":"1987","unstructured":"Aceto, L., De Nicola, R., Fantechi, A.: Testing equivalences for event structures. In: Zilli, M.V. (ed.) Mathematical Models for the Semantics of Parallelism. LNCS, vol. 280, pp. 1\u201320. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-18419-8_9"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Baumeister, J., Coenen, N., Bonakdarpour, B., Finkbeiner, B., S\u00e1nchez, C.: A temporal logic for asynchronous hyperproperties. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 694\u2013717. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_33","DOI":"10.1007\/978-3-030-81685-8_33"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Best, E., Fern\u00e1ndez, C.: Nonsequential Processes. Springer (1988). https:\/\/doi.org\/10.1007\/978-3-642-73483-0","DOI":"10.1007\/978-3-642-73483-0"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Best, E., Devillers, R.: Petri Net Primer \u2013 A Compendium of the Core Model, Analysis, and Synthesis. Computer Science Foundations and Applied Logic, Birkh\u00e4user (2024). https:\/\/doi.org\/10.1007\/978-3-031-48278-6","DOI":"10.1007\/978-3-031-48278-6"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B., Frenkel, H., Metzger, N.: Second-order hyperproperties. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Proc., Part II. LNCS, vol. 13965, pp. 309\u2013332. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7","DOI":"10.1007\/978-3-031-37703-7"},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Bozzelli, L., Peron, A., S\u00e1nchez, C.: Asynchronous extensions of HyperLTL. In: 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021, pp. 1\u201313. IEEE (2021).https:\/\/doi.org\/10.1109\/LICS52264.2021.9470583","DOI":"10.1109\/LICS52264.2021.9470583"},{"key":"9_CR7","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.) Principles of Security and Trust \u2013 Third International Conference, POST 2014, Held as Part of ETAPS 2014, Proceedings of the LNCS, vol.\u00a08414, pp. 265\u2013284. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8","DOI":"10.1007\/978-3-642-54792-8"},{"key":"9_CR8","doi-asserted-by":"crossref","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":"9_CR9","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., S\u00e1nchez, C., Tentrup, L.: Verifying hyperliveness. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 121\u2013139. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_7","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"De Nicola, R., Hennessy, M.: Testing equivalences for processes. TCS 34, 83\u2013134 (1984). https:\/\/doi.org\/10.1016\/0304-3975(84)90113-0","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-030-67067-2_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Dietsch","year":"2021","unstructured":"Dietsch, D., Heizmann, M., Klumpp, D., Naouar, M., Podelski, A., Sch\u00e4tzle, C.: Verification of concurrent programs using Petri net unfoldings. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI 2021. LNCS, vol. 12597, pp. 174\u2013195. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_9"},{"issue":"6","key":"9_CR12","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/BF01463946","volume":"28","author":"J Engelfriet","year":"1991","unstructured":"Engelfriet, J.: Branching processes of Petri nets. Acta Informatica 28(6), 575\u2013591 (1991). https:\/\/doi.org\/10.1007\/BF01463946","journal-title":"Acta Informatica"},{"key":"9_CR13","doi-asserted-by":"publisher","unstructured":"Esparza, J., Heljanko, K.: Unfoldings - A Partial-Order Approach to Model Checking. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-77426-6","DOI":"10.1007\/978-3-540-77426-6"},{"key":"9_CR14","first-page":"244","volume":"52","author":"J Esparza","year":"1994","unstructured":"Esparza, J., Nielsen, M.: Decidability issues for Petri nets - a survey. Bull. EATCS 52, 244\u2013262 (1994)","journal-title":"Bull. EATCS"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Farzan, A., Klumpp, D., Podelski, A.: Sound sequentialization for concurrent program verification. In: Jhala, R., Dillig, I. (eds.) PLDI \u201922: 43rd ACM SIGPLAN Intern. Conf. on Programming Language Design and Implementation, 2022. pp. 506\u2013521. ACM (2022). https:\/\/doi.org\/10.1145\/3519939.3523727","DOI":"10.1145\/3519939.3523727"},{"issue":"2","key":"9_CR16","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/3610392.3610394","volume":"10","author":"B Finkbeiner","year":"2023","unstructured":"Finkbeiner, B.: Logics and algorithms for hyperproperties. ACM SIGLOG News 10(2), 4\u201323 (2023). https:\/\/doi.org\/10.1145\/3610392.3610394","journal-title":"ACM SIGLOG News"},{"key":"9_CR17","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Olderog, E.R.: Concurrent hyperproperties. In: Bowen, J.P., Li, Q., Xu, Q. (eds.) Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday. LNCS, vol. 14080, pp. 211\u2013231. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-40436-8","DOI":"10.1007\/978-3-031-40436-8"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-319-21690-4_3","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2015","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL$$^*$$. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 30\u201348. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3"},{"issue":"6\u20138","key":"9_CR19","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1016\/J.IPL.2015.02.009","volume":"115","author":"O Finkel","year":"2015","unstructured":"Finkel, O.: The exact complexity of the infinite post correspondence problem. Inf. Process. Lett. 115(6\u20138), 609\u2013611 (2015). https:\/\/doi.org\/10.1016\/J.IPL.2015.02.009","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"9_CR20","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0020-0190(86)90058-X","volume":"22","author":"F Gire","year":"1986","unstructured":"Gire, F.: Two decidability problems for infinite words. Inf. Process. Lett. 22(3), 135\u2013140 (1986). https:\/\/doi.org\/10.1016\/0020-0190(86)90058-X","journal-title":"Inf. Process. Lett."},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proc. IEEE Symposium on Security and Privacy, pp. 11\u201320. IEEE Computer Society (1982). https:\/\/doi.org\/10.1109\/SP.1982.10014","DOI":"10.1109\/SP.1982.10014"},{"key":"9_CR22","doi-asserted-by":"publisher","unstructured":"Goltz, U.: On representing CCS programs by finite Petri nets. In: Chytil, M., Janiga, L., Koubek, V. (eds.) Proc. Math. Found. of Comput. Sci. 1988,. LNCS, vol.\u00a0324, pp. 339\u2013350. Springer (1988). https:\/\/doi.org\/10.1007\/BFb0017157","DOI":"10.1007\/BFb0017157"},{"key":"9_CR23","doi-asserted-by":"publisher","unstructured":"Goltz, U., Wehrheim, H.: Causal testing. In: Penczek, W., Szalas, A. (eds.) Mathematical Foundations of Computer Science 1996, 21st International Symposium, Proceedings LNCS, vol.\u00a01113, pp. 394\u2013406. Springer (1996). https:\/\/doi.org\/10.1007\/3-540-61550-4","DOI":"10.1007\/3-540-61550-4"},{"key":"9_CR24","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) (2021). https:\/\/doi.org\/10.1145\/3434319","DOI":"10.1145\/3434319"},{"key":"9_CR25","unstructured":"Hennessy, M.: Algebraic Theory of Processes. MIT Press (1988)"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Mantel, H., Reinhard, A.: Controlling the what and where of declassification in language-based security. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 141\u2013156. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71316-6_11","DOI":"10.1007\/978-3-540-71316-6_11"},{"issue":"3","key":"9_CR27","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1137\/0213029","volume":"13","author":"EW Mayr","year":"1984","unstructured":"Mayr, E.W.: An algorithm for the general Petri net reachability problem. SIAM J. Comput. 13(3), 441\u2013460 (1984). https:\/\/doi.org\/10.1137\/0213029","journal-title":"SIAM J. Comput."},{"key":"9_CR28","doi-asserted-by":"publisher","unstructured":"McCullough, D.: Noninterference and the composability of security properties. In: Proceedings IEEE Symposium on Security and Privacy, pp. 177\u2013186. IEEE Computer Society (1988). https:\/\/doi.org\/10.1109\/SECPRI.1988.8110","DOI":"10.1109\/SECPRI.1988.8110"},{"key":"9_CR29","doi-asserted-by":"publisher","unstructured":"McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pp. 79\u201393. IEEE Computer Society (1994). https:\/\/doi.org\/10.1109\/RISP.1994.296590","DOI":"10.1109\/RISP.1994.296590"},{"key":"9_CR30","doi-asserted-by":"publisher","unstructured":"Milner, R.: A Calculus of Communicating Systems, LNCS, vol.\u00a092. Springer (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3","DOI":"10.1007\/3-540-10235-3"},{"key":"9_CR31","doi-asserted-by":"publisher","unstructured":"Olderog, E.R.: Nets, Terms and Formulas: Three Views of Concurrent Processes and Their Relationship. Cambridge University Press (1991). https:\/\/doi.org\/10.1017\/CBO9780511526589","DOI":"10.1017\/CBO9780511526589"},{"key":"9_CR32","doi-asserted-by":"publisher","unstructured":"Olderog, E.R., Dierks, H.: Real-Time Systems - Formal Specification and Automatic Verification. Cambridge University Press (2008). https:\/\/doi.org\/10.1017\/CBO9780511619953","DOI":"10.1017\/CBO9780511619953"},{"key":"9_CR33","unstructured":"Petri, C.: Non-sequential processes. Tech. Rep. Internal Report GMD-ISF-77-5, Gesellschaft Math. Datenverarb., St. Augustin (1977)"},{"issue":"4","key":"9_CR34","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-642-19835-9","volume":"54","author":"EL Post","year":"1946","unstructured":"Post, E.L.: A variant of a recursively unsolvable problem. Bull. Am. Math. Soc. 54(4), 264\u2013268 (1946). https:\/\/doi.org\/10.1007\/978-3-642-19835-9","journal-title":"Bull. Am. Math. Soc."},{"key":"9_CR35","doi-asserted-by":"publisher","unstructured":"Pratt, V.: The pomset model of parallel processes: unifying the temporal and the spatial. In: Brookes, S.D., Roscoe, A.W., Winskel, G. (eds.) CONCURRENCY 1984. LNCS, vol. 197, pp. 180\u2013196. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/3-540-15670-4_9","DOI":"10.1007\/3-540-15670-4_9"},{"key":"9_CR36","doi-asserted-by":"publisher","unstructured":"Reisig, W.: Petri Nets - An Introduction. Springer (1985). https:\/\/doi.org\/10.1007\/978-3-642-69968-9","DOI":"10.1007\/978-3-642-69968-9"},{"issue":"12","key":"9_CR37","first-page":"579","volume":"21","author":"K Ruohonen","year":"1985","unstructured":"Ruohonen, K.: Reversible machines and Post\u2019s correspondence problem for biprefix morphisms. J. Inf. Process. Cybern. 21(12), 579\u2013595 (1985)","journal-title":"J. Inf. Process. Cybern."},{"issue":"5","key":"9_CR38","doi-asserted-by":"publisher","first-page":"517","DOI":"10.3233\/JCS-2009-0352","volume":"17","author":"A Sabelfeld","year":"2009","unstructured":"Sabelfeld, A., Sands, D.: Declassification: dimensions and principles. J. Comput. Secur. 17(5), 517\u2013548 (2009). https:\/\/doi.org\/10.3233\/JCS-2009-0352","journal-title":"J. Comput. Secur."},{"key":"9_CR39","doi-asserted-by":"publisher","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: 16th IEEE Computer Security Foundations Workshop (CSFW-16 2003), pp. 29\u201343. IEEE Computer Society (2003). https:\/\/doi.org\/10.1109\/CSFW.2003.1212703","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Lecture Notes in Computer Science","On the Pursuit of Insight and Elegance"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-13711-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T06:41:32Z","timestamp":1767768092000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-13711-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032137104","9783032137111"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-13711-1_9","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":"8 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}