{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:51:49Z","timestamp":1760043109171,"version":"3.41.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"DFG","award":["MU 1508\/3"],"award-info":[{"award-number":["MU 1508\/3"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>We introduce a novel logic for asynchronous hyperproperties with a new mechanism to identify relevant positions on traces. While the new logic is more expressive than a related logic presented recently by Bozzelli et al., we obtain the same complexity of the model checking problem for finite state models. Beyond this, we study the model checking problem of our logic for pushdown models. We argue that the combination of asynchronicity and a non-regular model class studied in this paper constitutes the first suitable approach for hyperproperty model checking against recursive programs.<\/jats:p>","DOI":"10.1145\/3632844","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"33-60","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Deciding Asynchronous Hyperproperties for Recursive Programs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-5806-441X","authenticated-orcid":false,"given":"Jens Oliver","family":"Gutsfeld","sequence":"first","affiliation":[{"name":"University of M\u00fcnster, M\u00fcnster, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-2229-9651","authenticated-orcid":false,"given":"Markus","family":"M\u00fcller-Olm","sequence":"additional","affiliation":[{"name":"University of M\u00fcnster, M\u00fcnster, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-1813-4596","authenticated-orcid":false,"given":"Christoph","family":"Ohrem","sequence":"additional","affiliation":[{"name":"University of M\u00fcnster, M\u00fcnster, Germany"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_35"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007352.1007390"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_16"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_33"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_17"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-55754-6_18"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03421-4_2"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63141-0_10"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_32"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"Laura Bozzelli Adriano Peron and C\u00e9sar S\u00e1nchez. 2021. Asynchronous Extensions of HyperLTL. In 36th Annual ACM\/IEEE Symposium on Logic in Computer Science LICS 2021 Rome Italy June 29 - July 2 2021. IEEE 1\u201313. https:\/\/doi.org\/10.1109\/LICS52264.2021.9470583 10.1109\/LICS52264.2021.9470583","DOI":"10.1109\/LICS52264.2021.9470583"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2022.27"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0056"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","unstructured":"Michael R. Clarkson and Fred B. Schneider. 2010. Hyperproperties. J. Comput. Secur. 18 6 (Sept. 2010) 1157\u20131210. https: \/\/doi.org\/10.3233\/JCS-2009-0393 10.3233\/JCS-2009-0393","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785713"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Christian Dax and Felix Klaedtke. 2008. Alternation elimination by complementation. In International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer 214\u2013229. https:\/\/doi.org\/10.1007\/978-3-540-89439-1_16 10.1007\/978-3-540-89439-1_16","DOI":"10.1007\/978-3-540-89439-1_16"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","unstructured":"St\u00e9phane Demri Valentin Goranko and Martin Lange. 2016. Temporal Logics in Computer Science: Finite-State Systems. Cambridge University Press. https:\/\/doi.org\/10.1017\/CBO9781139236119 10.1017\/CBO9781139236119","DOI":"10.1017\/CBO9781139236119"},{"key":"e_1_3_1_19_1","article-title":"Temporal Hyperproperties","volume":"123","author":"Finkbeiner Bernd","year":"2017","unstructured":"Bernd Finkbeiner. 2017. Temporal Hyperproperties. Bulletin of the EATCS 123 (2017).","journal-title":"Bulletin of the EATCS"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","unstructured":"Bernd Finkbeiner Markus N. Rabe and C\u00e9sar S\u00e1nchez. 2015. Algorithms for Model Checking HyperLTL and HyperCTL*. In CAV 2015. 30\u201348. https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3 10.1007\/978-3-319-21690-4_3","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533360"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2020.50"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434319"},{"key":"e_1_3_1_24_1","unstructured":"Jens Oliver Gutsfeld Markus M\u00fcller-Olm and Christoph Ohrem. 2023. Deciding Asynchronous Hyperproperties for Recursive Programs. arXiv:2201.12859 [cs.LO] https:\/\/arxiv.org\/abs\/2201.12859"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.MFCS.2018.10"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94111-0_8"},{"key":"e_1_3_1_27_1","unstructured":"Markus N. Rabe. 2016. A temporal logic approach to Information-flow control. Ph.D. Dissertation. Saarland University."},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.73.5"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73582"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2021.52"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","unstructured":"Pierre Wolper. 1981. Temporal Logic Can Be More Expressive. In 22nd Annual Symposium on Foundations of Computer Science Nashville Tennessee USA 28-30 October 1981. IEEE Computer Society 340\u2013348. https:\/\/doi.org\/10.1109\/SFCS.1981.44 10.1109\/SFCS.1981.44","DOI":"10.1109\/SFCS.1981.44"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632844","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632844","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:06:16Z","timestamp":1751659576000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632844"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":31,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632844"],"URL":"https:\/\/doi.org\/10.1145\/3632844","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}