{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:21:49Z","timestamp":1778498509661,"version":"3.51.4"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031404351","type":"print"},{"value":"9783031404368","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,8]],"date-time":"2023-09-08T00:00:00Z","timestamp":1694131200000},"content-version":"vor","delay-in-days":250,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Trace properties, which are sets of execution traces, are often used to analyze systems, but their expressiveness is limited. Clarkson and Schneider defined <jats:italic>hyperproperties<\/jats:italic> as a generalization of trace properties to sets of sets of traces. Typical applications of hyperproperties are found in information flow security. We introduce an analogous definition of <jats:italic>concurrent<\/jats:italic> hyperproperties, by generalizing traces to <jats:italic>concurrent<\/jats:italic> traces, which we define as partially ordered multisets. We take Petri nets as the basic semantic model. Concurrent traces are formalized via causal nets. To check concurrent hyperproperties, we define <jats:italic>may<\/jats:italic> and <jats:italic>must testing<\/jats:italic> of sets of concurrent traces in the style of DeNicola and Hennessy, using the parallel composition of Petri nets. In our approach, we thus distinguish nondeterministic and concurrent behavior. We discuss examples where concurrent hyperproperties are needed.<\/jats:p>","DOI":"10.1007\/978-3-031-40436-8_8","type":"book-chapter","created":{"date-parts":[[2023,9,7]],"date-time":"2023-09-07T23:04:03Z","timestamp":1694127843000},"page":"211-231","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Concurrent 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":[[2023,9,8]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Aichernig, B.K., He, J.: Refinement and test case generation in UTP. In: Aichernig, B.K., Boiten, E.A., Derrick, J., Groves, L. (eds.) Proceedings of the 11th Refinement Workshop, Refine@ICFEM 2006, Macao. Electronic Notes in Theoretical Computer Science, vol. 187, pp. 125\u2013143. Elsevier (2006). https:\/\/doi.org\/10.1016\/j.entcs.2006.08.048","DOI":"10.1016\/j.entcs.2006.08.048"},{"key":"8_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-73483-0","volume-title":"Nonsequential Processes","author":"E Best","year":"1988","unstructured":"Best, E., Fern\u00e1ndez, C.: Nonsequential Processes. Springer, Berlin (1988). https:\/\/doi.org\/10.1007\/978-3-642-73483-0"},{"issue":"6","key":"8_CR3","doi-asserted-by":"publisher","first-page":"1065","DOI":"10.1017\/S0960129509990120","volume":"19","author":"N Busi","year":"2009","unstructured":"Busi, N., Gorrieri, R.: Structural non-interference in elementary and trace nets. Math. Struct. Comput. Sci. 19(6), 1065\u20131090 (2009). https:\/\/doi.org\/10.1017\/S0960129509990120","journal-title":"Math. Struct. Comput. Sci."},{"issue":"6","key":"8_CR4","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010). https:\/\/doi.org\/10.3233\/JCS-2009-0393","journal-title":"J. Comput. Secur."},{"key":"8_CR5","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","volume":"34","author":"R DeNicola","year":"1984","unstructured":"DeNicola, R., Hennessy, M.: Testing equivalences for processes. TCS 34, 83\u2013134 (1984). https:\/\/doi.org\/10.1016\/0304-3975(84)90113-0","journal-title":"TCS"},{"key":"8_CR6","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":"8_CR7","unstructured":"Finkbeiner, B.: Temporal hyperproperties. Bull. EATCS 123 (2017). http:\/\/eatcs.org\/beatcs\/index.php\/beatcs\/article\/view\/514"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proceedings of the 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":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/BFb0017157","volume-title":"Mathematical Foundations of Computer Science 1988","author":"U Goltz","year":"1988","unstructured":"Goltz, U.: On representing CCS programs by finite petri nets. In: Chytil, M.P., Koubek, V., Janiga, L. (eds.) MFCS 1988. LNCS, vol. 324, pp. 339\u2013350. Springer, Heidelberg (1988). https:\/\/doi.org\/10.1007\/BFb0017157"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/3-540-58468-4_171","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J He","year":"1994","unstructured":"He, J., et al.: Provably correct systems. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994. LNCS, vol. 863, pp. 288\u2013335. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58468-4_171"},{"key":"8_CR11","volume-title":"Algebraic Theory of Processes","author":"M Hennessy","year":"1988","unstructured":"Hennessy, M.: Algebraic Theory of Processes. MIT Press, Cambridge (1988)"},{"key":"8_CR12","volume-title":"Unifying Theories of Programming","author":"CAR Hoare","year":"1998","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, Hoboken (1998)"},{"key":"8_CR13","unstructured":"Hoare, C.: A model for communicating sequential processes. In: McKeag, R., MacNaughten, A. (eds.) On the Construction of Programs, pp. 229\u2013254. Cambridge University Press (1980)"},{"issue":"3","key":"8_CR14","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":"8_CR15","doi-asserted-by":"publisher","unstructured":"Mazurkiewicz, A.: Concurrent program schemes and their interpretations. DAIMI Rep. Ser. 6(78) (1977). https:\/\/doi.org\/10.7146\/dpb.v6i78.7691","DOI":"10.7146\/dpb.v6i78.7691"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"McCullough, D.: Noninterference and the composability of security properties. In: Proceedings of the 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":"8_CR17","doi-asserted-by":"publisher","unstructured":"Milner, R.: A Calculus of Communicating Systems, LNCS, vol. 92. Springer, Berlin (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3, http:\/\/link.springer.com\/10.1007\/3-540-10235-3","DOI":"10.1007\/3-540-10235-3"},{"issue":"1","key":"8_CR18","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0304-3975(92)90181-E","volume":"96","author":"M Mukund","year":"1992","unstructured":"Mukund, M., Thiagarajan, P.S.: A logical characterization of well branching event structures. Theor. Comput. Sci. 96(1), 35\u201372 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90181-E","journal-title":"Theor. Comput. Sci."},{"key":"8_CR19","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526589","volume-title":"Nets, Terms and Formulas: Three Views of Concurrent Processes and Their Relationship","author":"ER Olderog","year":"1991","unstructured":"Olderog, E.R.: Nets, Terms and Formulas: Three Views of Concurrent Processes and Their Relationship. Cambridge University Press, Cambridge (1991). https:\/\/doi.org\/10.1017\/CBO9780511526589"},{"key":"8_CR20","unstructured":"Penczek, W.: Branching time and partial order in temporal logics. In: Bolc, L., Szalas, A. (eds.) Time and Logics: A Computational Approach, pp. 203\u2013257. UCL Press Ltd. (1995)"},{"key":"8_CR21","unstructured":"Petri, C.: Non-sequential processes. Technical Report. Internal Report GMD-ISF-77-5, Gesellschaft Math. Datenverarb., St. Augustin (1977)"},{"issue":"4","key":"8_CR22","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":"8_CR23","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/3-540-15670-4","volume-title":"Seminar on Concurrency","author":"VR Pratt","year":"1985","unstructured":"Pratt, V.R.: 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"},{"key":"8_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69968-9","volume-title":"Petri Nets - An Introduction","author":"W Reisig","year":"1985","unstructured":"Reisig, W.: Petri Nets - An Introduction. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/978-3-642-69968-9"},{"key":"8_CR25","doi-asserted-by":"publisher","unstructured":"Su, T., Fu, Z., Pu, G., He, J., Su, Z.: Combining symbolic execution and model checking for data flow testing. In: Bertolino, A., Canfora, G., Elbaum, S.G. (eds.) 37th IEEE\/ACM International Conference on Software Engineering, ICSE 2015, vol. 1, pp. 654\u2013665. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/ICSE.2015.81","DOI":"10.1109\/ICSE.2015.81"},{"key":"8_CR26","doi-asserted-by":"publisher","unstructured":"Su, T., et al.: A survey on data-flow testing. ACM Comput. Surv. 50(1), 5:1\u20135:35 (2017). https:\/\/doi.org\/10.1145\/3020266","DOI":"10.1145\/3020266"},{"key":"8_CR27","unstructured":"Winskel, G.: Event structures: Lecture notes for the Advanced Course on Petri Nets. Technical Report UCAM-CL-TR-95, University of Cambridge, Computer Laboratory (1986). https:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-95.pdf"}],"container-title":["Lecture Notes in Computer Science","Theories of Programming and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-40436-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,7]],"date-time":"2023-09-07T23:06:16Z","timestamp":1694127976000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-40436-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031404351","9783031404368"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-40436-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"8 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}