{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:20:51Z","timestamp":1776316851496,"version":"3.50.1"},"reference-count":45,"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>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-04T17:34:24Z","timestamp":1609781664000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"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"}]},{"given":"Markus","family":"M\u00fcller-Olm","sequence":"additional","affiliation":[{"name":"University of M\u00fcnster, Germany"}]},{"given":"Christoph","family":"Ohrem","sequence":"additional","affiliation":[{"name":"University of M\u00fcnster, Germany"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"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.2019.8785713"},{"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.1991.185392"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2842603"},{"key":"e_1_2_1_16_1","unstructured":"Bernd Finkbeiner. 2017. Temporal Hyperproperties. Bulletin of the EATCS 123 ( 2017 ).  Bernd Finkbeiner. 2017. Temporal Hyperproperties. Bulletin of the EATCS 123 ( 2017 )."},{"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","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.2016.05.005"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2009.09.002"},{"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  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.2020.50"},{"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] 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.2018.10"},{"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","DOI":"10.1016\/S0304-3975(96)00117-X"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00314-4"},{"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_43_1","doi-asserted-by":"publisher","DOI":"10.1147\/rd.32.0114"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.73.5"},{"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.  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":[[2025,6,17]],"date-time":"2025-06-17T21:24:35Z","timestamp":1750195475000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434319"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":45,"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":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}