{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:53:41Z","timestamp":1781855621546,"version":"3.54.5"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["MU 1508\/3"],"award-info":[{"award-number":["MU 1508\/3"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>\n                    Hyperproperties have received increasing attention in the last decade due to their importance e.g. for security analyses. Past approaches have focussed on synchronous analyses, i.e. techniques in which different paths are compared lockstepwise. In this paper, we systematically study asynchronous analyses for hyperproperties by introducing both a novel automata model (Alternating Asynchronous Parity Automata) and the temporal fixpoint calculus\n                    <jats:italic toggle=\"yes\">H<\/jats:italic>\n                    <jats:sub>\u00b5<\/jats:sub>\n                    , the first fixpoint calculus that can systematically express hyperproperties in an asynchronous manner and at the same time subsumes the existing logic HyperLTL. We show that the expressive power of both models coincides over fixed path assignments. The high expressive power of both models is evidenced by the fact that decision problems of interest are highly undecidable, i.e. not even arithmetical. As a remedy, we propose approximative analyses for both models that also induce natural decidable fragments.\n                  <\/jats:p>","DOI":"10.1145\/3434319","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["Automata and fixpoints for asynchronous hyperproperties"],"prefix":"10.1145","volume":"5","author":[{"given":"Jens Oliver","family":"Gutsfeld","sequence":"first","affiliation":[{"name":"University of M\u00fcnster, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Markus","family":"M\u00fcller-Olm","sequence":"additional","affiliation":[{"name":"University of M\u00fcnster, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"Ohrem","sequence":"additional","affiliation":[{"name":"University of M\u00fcnster, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Henrik Reif Andersen. 1994. A polyadic modal-calculus. Technical Report ID-TR: 1994-195. Dept. of Computer Science Technical University of Denmark Copenhagen."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_11"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38536-0_35"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512660"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_32"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_11"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1979.82.43"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_16"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139236119"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_5"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2842603"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Bernd Finkbeiner. 2017. Temporal Hyperproperties. Bulletin of the EATCS 123 ( 2017 ).","DOI":"10.1007\/978-3-319-67531-2_12"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2016.13"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-019-00358-2"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","unstructured":"Bernd Finkbeiner Christopher Hahn Marvin Stenger and Leander Tentrup. 2019. Monitoring hyperproperties. Formal Methods Syst. Des. 54 3 ( 2019 ) 336-363. https:\/\/doi.org\/10.1007\/s10703-019-00334-z 10.1007\/s10703-019-00334-z","DOI":"10.1007\/s10703-019-00334-z"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/11672142_24"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl"},{"key":"e_1_2_1_24_1","unstructured":"Carlo A. Furia. 2014. Asynchronous Multi-Tape Automata Intersection: Undecidabiliy and Approximation. CoRR abs\/1206.4860 ( 2014 ). arXiv: 1206.4860v5 http:\/\/arxiv.org\/abs\/1206.4860v5"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160915"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480895"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-18740-5_35"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR"},{"key":"e_1_2_1_29_1","volume-title":"Automata and Fixpoints for Asynchronous Hyperproperties. arXiv","author":"Gutsfeld Jens Oliver","year":"2010","unstructured":"Jens Oliver Gutsfeld, Markus M\u00fcller-Olm, and Christoph Ohrem. 2020b. Automata and Fixpoints for Asynchronous Hyperproperties. arXiv: 2010. 11605 [cs.LO]"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054113400194"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.MFCS"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_18"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.191.10"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_12"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99725-4_17"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41488-6_17"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","unstructured":"Anca Muscholl. 1996. On the Complementation of Asynchronous Cellular B\u00fcchi Automata. Theor. Comput. Sci. 169 2 ( 1996 ) 123-145. https:\/\/doi.org\/10.1016\/S0304-3975 ( 96 ) 00117-X 10.1016\/S0304-3975(96)00117-X","DOI":"10.1016\/S0304-3975"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-34892-6_20"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85114-1_2"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_2_1_42_1","unstructured":"Markus N. Rabe. 2016. A temporal logic approach to Information-flow control. Ph.D. Dissertation. Saarland University."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1147\/rd.32.0114"},{"key":"e_1_2_1_44_1","unstructured":"Aravinda Prasad Sistla. 1983. Theoretical Issues in the Design and Verification of Distributed Systems. Ph.D. Dissertation. Carnegie-Mellon University USA."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.73.5"},{"key":"e_1_2_1_46_1","unstructured":"Larry Joseph Stockmeyer. 1974. The complexity of decision problems in automata theory and logic. Ph.D. Dissertation. MIT."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.735822"},{"key":"e_1_2_1_49_1","doi-asserted-by":"crossref","unstructured":"Wieslaw Zielonka. 1987. Notes on Finite Asynchronous Automata. ITA 21 2 ( 1987 ) 99-135.","DOI":"10.1051\/ita\/1987210200991"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434319","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434319","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:25:24Z","timestamp":1781853924000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434319"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":49,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434319"],"URL":"https:\/\/doi.org\/10.1145\/3434319","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}