{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,15]],"date-time":"2026-07-15T15:04:49Z","timestamp":1784127889749,"version":"3.55.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2026,7,15]],"date-time":"2026-07-15T00:00:00Z","timestamp":1784073600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"BLOQUES-CM","award":["S2018\/TCS-4339"],"award-info":[{"award-number":["S2018\/TCS-4339"]}]},{"name":"TMCIN\/AEI","award":["TED2021-132464B-I00"],"award-info":[{"award-number":["TED2021-132464B-I00"]}]},{"name":"MCIN\/AEI","award":["10.13039\/501100011033"],"award-info":[{"award-number":["10.13039\/501100011033"]}]},{"DOI":"10.13039\/501100004895","name":"European Social Fund Plus","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004895","id-type":"DOI","asserted-by":"crossref"}]},{"name":"MICIU\/AEI","award":["10.13039\/501100011033"],"award-info":[{"award-number":["10.13039\/501100011033"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2026,7,31]]},"abstract":"<jats:p>\n                    Hyperproperties are a modern specification paradigm that extends properties of a single trace to express properties of a set of traces. Temporal logics for hyperproperties studied in the literature, including HyperLTL, assume a synchronous semantics and enjoy a decidable model checking problem. In this article, we introduce two asynchronous and orthogonal extensions of HyperLTL,\n                    <jats:italic toggle=\"yes\">Stuttering HyperLTL<\/jats:italic>\n                    (HyperLTL\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\({}_{S}\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    ) and\n                    <jats:italic toggle=\"yes\">Context HyperLTL<\/jats:italic>\n                    (HyperLTL\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\({}_{C}\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    ). Both of these extensions are useful, for instance, to formulate asynchronous variants of information-flow security properties. We show that for these logics, model checking is in general undecidable. On the positive side, for each of them, we identify a fragment with a decidable model checking problem that subsumes HyperLTL and that can express meaningful asynchronous requirements. Moreover, we provide the exact computational complexity of model checking for these two fragments which, for the HyperLTL\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\({}_{S}\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    fragment, coincides with that of the strictly less expressive logic HyperLTL.\n                  <\/jats:p>","DOI":"10.1145\/3815107","type":"journal-article","created":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T14:25:16Z","timestamp":1779805516000},"page":"1-40","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Extensions of HyperLTL for Asynchronous Hyperproperties"],"prefix":"10.1145","volume":"27","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-8555-8229","authenticated-orcid":false,"given":"Laura","family":"Bozzelli","sequence":"first","affiliation":[{"name":"DINF, Pegaso Telematic University, Naples, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7111-3171","authenticated-orcid":false,"given":"Adriano","family":"Peron","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Trieste, Trieste, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3927-4773","authenticated-orcid":false,"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Pozuelo de Alarcon, Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,7,15]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"333","volume-title":"Proceedings of the 13th European Symposium on Research in Computer Security Computer Security (ESORICS)","author":"Askarov A.","year":"2008","unstructured":"A. Askarov, S. Hunt, A. Sabelfeld, and D. Sands. 2008. Termination-insensitive noninterference leaks more than just a bit. In Proceedings of the 13th European Symposium on Research in Computer Security Computer Security (ESORICS), 333\u2013348."},{"key":"e_1_3_2_3_2","first-page":"694","volume-title":"Proceedings of the 33rd International Conference on Computer Aided Verifiation (CAV), LNCS, Vol","volume":"12759","author":"Baumeister J.","year":"2021","unstructured":"J. Baumeister, N. Coenen, B. Bonakdarpour, B. Finkbeiner, and C. S\u00e1nchez. 2021. A temporal logic for asynchronous hyperproperties. In Proceedings of the 33rd International Conference on Computer Aided Verifiation (CAV), LNCS, Vol. 12759. Springer, 694\u2013717. DOI: 10.1007\/978-3-030-81685-8_33"},{"key":"e_1_3_2_4_2","first-page":"341","volume-title":"Proceedings of the 34th International Conference on Computer Aided Verifiation (CAV)","volume":"13371","author":"Beutner Raven","year":"2022","unstructured":"Raven Beutner and Bernd Finkbeiner. 2022. Software verification of hyperproperties beyond k-safety. In Proceedings of the 34th International Conference on Computer Aided Verifiation (CAV), LNCS, Vol. 13371. Springer, 341\u2013362."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3763130"},{"key":"e_1_3_2_6_2","first-page":"309","volume-title":"Proceedings of the 35th International Conference on Computer Aided Verifiation (CAV)","volume":"13965","author":"Beutner R.","year":"2023","unstructured":"R. Beutner, B. Finkbeiner, H. Frenkel, and N. Metzger. 2023. Second-order hyperproperties. In Proceedings of the 35th International Conference on Computer Aided Verifiation (CAV), Lecture Notes in Computer Science, Vol. 13965, Springer, 309\u2013332. DOI: 10.1007\/978-3-031-37703-7_15"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.ARTINT.2022.103725"},{"key":"e_1_3_2_8_2","first-page":"8","volume-title":"Proceedings of the 8th Annual Conference of The Indian Society of Landscape Architects (ISoLA)","volume":"11245","author":"Bonakdarpour B.","year":"2018","unstructured":"B. Bonakdarpour, C. S\u00e1nchez, and G. Schneider. 2018. Monitoring hyperproperties by combining static analysis and runtime verification. In Proceedings of the 8th Annual Conference of The Indian Society of Landscape Architects (ISoLA), LNCS, Vol. 11245. Springer, 8\u201327. DOI: 10.1007\/978-3-030-03421-4_2"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(4:4)2015"},{"key":"e_1_3_2_10_2","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-662-46678-0_11","volume-title":"Proceedings of the 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)","volume":"9034","author":"Bozzelli L.","year":"2015","unstructured":"L. Bozzelli, B. Maubert, and S. Pinchinat. 2015. Unifying hyper and epistemic temporal logics. In Proceedings of the 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), LNCS, Vol. 9034. Springer, 167\u2013182. DOI: 10.1007\/978-3-662-46678-0_11"},{"key":"e_1_3_2_11_2","first-page":"1","volume-title":"Proceedings of the 36th International Symposium on Logic in Computer Science (LICS)","author":"Bozzelli L.","year":"2021","unstructured":"L. Bozzelli, A. Peron, and C. S\u00e1nchez. 2021. Asynchronous extensions of HyperLTL. In Proceedings of the 36th International Symposium on Logic in Computer Science (LICS). IEEE, 1\u201313. DOI: 10.1109\/LICS52264.2021.9470583"},{"key":"e_1_3_2_12_2","first-page":"1","volume-title":"Proceedings of the 33rd International Conference on Concurrency Theory (CONCUR)","volume":"243","author":"Bozzelli L.","year":"2022","unstructured":"L. Bozzelli, A. Peron, and C. S\u00e1nchez. 2022. Expressiveness and decidability of temporal logics for asynchronous hyperproperties. In Proceedings of the 33rd International Conference on Concurrency Theory (CONCUR), LIPIcs, Vol. 243, Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, Article 27, 1\u201316. DOI: 10.4230\/LIPIcs.CONCUR.2022.27"},{"key":"e_1_3_2_13_2","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proceedings of the Logics of Programs","volume":"131","author":"Clarke E. M.","year":"1981","unstructured":"E. M. Clarke and E. A. Emerson. 1981. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings of the Logics of Programs, LNCS, Vol. 131, 52\u201371. DOI: 10.1007\/BFb0025774"},{"key":"e_1_3_2_14_2","first-page":"265","volume-title":"Proceedings of the 3rd POST","volume":"8414","author":"Clarkson M. R.","year":"2014","unstructured":"M. R. Clarkson, B. Finkbeiner, M. Koleini, K. K. Micinski, M. N. Rabe, and C. S\u00e1nchez. 2014. Temporal logics for hyperproperties. In Proceedings of the 3rd POST, LNCS, Vol. 8414, Springer, 265\u2013284. DOI: 10.1007\/978-3-642-54792-8_15"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_2_16_2","first-page":"1","volume-title":"Proceedings of the 34th International Symposium on Logic in Computer Science (LICS)","author":"Coenen N.","year":"2019","unstructured":"N. Coenen, B. Finkbeiner, C. Hahn, and J. Hofmann. 2019. The hierarchy of hyperlogics. In Proceedings of the 34th International Symposium on Logic in Computer Science (LICS). IEEE, 1\u201313. DOI: 10.1109\/LICS.2019.8785713"},{"key":"e_1_3_2_17_2","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/978-3-642-27940-9_12","volume-title":"Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)","volume":"7148","author":"Dimitrova R.","year":"2012","unstructured":"R. Dimitrova, B. Finkbeiner, M. Kov\u00e1cs, M. N. Rabe, and H. Seidl. 2012. Model checking information flow in reactive systems. In Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS, Vol. 7148, Springer, 169\u2013185. DOI: 10.1007\/978-3-642-27940-9_12"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_3_2_19_2","first-page":"1","article-title":"Temporal hyperproperties","volume":"123","author":"Finkbeiner B.","year":"2017","unstructured":"B. Finkbeiner. 2017. Temporal hyperproperties. Bulletin of EATCS 123 (2017), 1\u201322.","journal-title":"Bulletin of EATCS"},{"key":"e_1_3_2_20_2","first-page":"1","volume-title":"Proceedings of the 27th Conference on Concurrency Theory (CONCUR)","volume":"59","author":"Finkbeiner B.","year":"2016","unstructured":"B. Finkbeiner and C. Hahn. 2016. Deciding hyperproperties. In Proceedings of the 27th Conference on Concurrency Theory (CONCUR), LIPIcs, Vol. 59, Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, Article 13, 1\u201314. DOI: 10.4230\/LIPIcs.CONCUR.2016.13"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-019-00358-2"},{"key":"e_1_3_2_22_2","first-page":"30","volume-title":"Proceedings of the 27th International Conference on Computer Aided Verification (CAV), Part I","volume":"9206","author":"Finkbeiner B.","year":"2015","unstructured":"B. Finkbeiner, M. N. Rabe, and C. S\u00e1nchez. 2015. Algorithms for model checking HyperLTL and HyperCTL \\({}^{*}\\) . In Proceedings of the 27th International Conference on Computer Aided Verification (CAV), Part I, LNCS, Vol. 9206. Springer, 30\u201348. DOI: 10.1007\/978-3-319-21690-4_3"},{"key":"e_1_3_2_23_2","first-page":"1","volume-title":"Proceedings of the 34th International Symposium on Theoretical Aspects of Computer Science (STACS)","volume":"66","author":"Finkbeiner B.","year":"2017","unstructured":"B. Finkbeiner and M. Zimmermann. 2017. The first-order logic of hyperproperties. In Proceedings of the 34th International Symposium on Theoretical Aspects of Computer Science (STACS), LIPIcs, Vol. 66, Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, Article 30, 1\u201314. DOI: 10.4230\/LIPIcs.STACS.2017.30"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"e_1_3_2_25_2","first-page":"11","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy","author":"Goguen J. A.","year":"1982","unstructured":"J. A. Goguen and J. Meseguer. 1982. Security policies and security models. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 11\u201320. DOI: 10.1109\/SP.1982.10014"},{"key":"e_1_3_2_26_2","first-page":"1","volume-title":"Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science\u00b7(LICS)","volume":"44","author":"Gutsfeld JOliver","year":"2022","unstructured":"JOliver Gutsfeld, A. Meier, C. Ohrem, and J. Virtema. 2022. Temporal team semantics revisited. In Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science\u00b7(LICS). ACM, Article 44, 1\u201313. DOI: 10.1145\/3531130.3533360"},{"key":"e_1_3_2_27_2","first-page":"1","volume-title":"Proceedings of the 31st International Conference on Concurrency Theory (CONCUR)","volume":"171","author":"Oliver. Gutsfeld J.","year":"2020","unstructured":"J. Oliver. Gutsfeld, M. M\u00fcller-Olm, and C. Ohrem. 2020. Propositional dynamic logic for hyperproperties. In Proceedings of the 31st International Conference on Concurrency Theory (CONCUR), LIPIcs, Vol. 171, Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, Article 50, 1\u201322. DOI: 10.4230\/LIPIcs.CONCUR.2020.50"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434319"},{"issue":"1","key":"e_1_3_2_29_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1410234.1410239","article-title":"Secrecy in multiagent systems","volume":"12","author":"Halpern Joseph Y.","year":"2008","unstructured":"Joseph Y. Halpern and Kevin R. O\u2019Neill. 2008. Secrecy in multiagent systems. ACM Transactions on Information and System Security 12, 1 (2008), 1\u201347.","journal-title":"ACM Transactions on Information and System Security"},{"key":"e_1_3_2_30_2","volume-title":"Introduction to Automata Theory, Languages and Computation","author":"Hopcroft J. E.","year":"1979","unstructured":"J. E. Hopcroft and J. D. Ullman. 1979. Introduction to Automata Theory, Languages and Computation. Addison-Wesley."},{"key":"e_1_3_2_31_2","first-page":"29","volume-title":"Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201923)","volume":"13993","author":"Hsu Tzu-Han","year":"2023","unstructured":"Tzu-Han Hsu, Borzoo Bonakdarpour, Bernd Finkbeiner, and C\u00e9sar S\u00e1nchez. 2023. Bounded model checking for asynchronous hyperproperties. In Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201923), LNCS, Vol. 13993. Springer, 29\u201346. DOI: 10.1007\/978-3-031-30823-9_2"},{"key":"e_1_3_2_32_2","first-page":"1","volume-title":"Proceedings of the 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS)","volume":"10","author":"Krebs A.","year":"2018","unstructured":"A. Krebs, A. Meier, J. Virtema, and M. Zimmermann. 2018. Team semantics for the specification and verification of hyperproperties. In Proceedings of the 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS), LIPIcs, Vol. 117, Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, Article 10, 1\u201316. DOI: 10.4230\/LIPIcs.MFCS.2018.10"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0067-z"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2020.04.019"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.481534"},{"key":"e_1_3_2_36_2","volume-title":"Computation: Finite and Infinite Machines","author":"Minsky M. L.","year":"1967","unstructured":"M. L. Minsky. 1967. Computation: Finite and Infinite Machines. Prentice-Hall, Inc."},{"key":"e_1_3_2_37_2","first-page":"46","volume-title":"Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS)","author":"Pnueli A.","year":"1977","unstructured":"A. Pnueli. 1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS). IEEE Computer Society, 46\u201357. DOI: 10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_38_2","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"Proceedings of the 5th International Symposium on Programming","volume":"137","author":"Queille J. P.","year":"1982","unstructured":"J. P. Queille and J. Sifakis. 1982. Specification and verification of concurrent programs in CESAR. In Proceedings of the 5th International Symposium on Programming, LNCS, Vol. 137. Springer, 337\u2013351. DOI: 10.1007\/3-540-11494-7_22"},{"key":"e_1_3_2_39_2","unstructured":"M.N. Rabe. 2016. A Temporal Logic Approach to Information-Flow Control. Ph.D. Dissertation. Saarland University."},{"issue":"1","key":"e_1_3_2_40_2","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1023\/A:1011553200337","article-title":"A per model of secure information flow in sequential programs","volume":"14","author":"Sabelfeld A.","year":"2001","unstructured":"A. Sabelfeld and D. Sands. 2001. A per model of secure information flow in sequential programs. Higher-Order and Symbolic Computation 14, 1 (2001), 59\u201391.","journal-title":"Higher-Order and Symbolic Computation"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/9.412626"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"e_1_3_2_43_2","doi-asserted-by":"crossref","first-page":"432","DOI":"10.1007\/3-540-46691-6_35","volume-title":"Proceedings of the 19th Foundations of Software Technology and Theoretical Computer Science (FSTTCS)","author":"van der Meyden R.","year":"1999","unstructured":"R. van der Meyden and N. V. Shilov. 1999. Model checking knowledge and time in systems with perfect recall (extended abstract). In Proceedings of the 19th Foundations of Software Technology and Theoretical Computer Science (FSTTCS), LNCS, Vol. 1738, Springer, 432\u2013445."},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1092"},{"key":"e_1_3_2_45_2","first-page":"1","volume-title":"Proceedings of the 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)","volume":"213","author":"Virtema J.","year":"2021","unstructured":"J. Virtema, J. Hofmann, B. Finkbeiner, J. Kontinen, and F. Yang. 2021. Linear-time temporal logic with team semantics: Expressivity and complexity. In Proceedings of the 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), LIPIcs, Vol. 213, Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, Article 52, 1\u201317. DOI: 10.4230\/LIPIcs.FSTTCS.2021.52"},{"key":"e_1_3_2_46_2","first-page":"29","volume-title":"Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW)","author":"Zdancewic S.","year":"2003","unstructured":"S. Zdancewic and A. C. Myers. 2003. Observational determinism for concurrent program security. In Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW). IEEE Computer Society, 29\u201343. DOI: 10.1109\/CSFW.2003.1212703"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3815107","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,15]],"date-time":"2026-07-15T14:19:16Z","timestamp":1784125156000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3815107"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7,15]]},"references-count":45,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2026,7,31]]}},"alternative-id":["10.1145\/3815107"],"URL":"https:\/\/doi.org\/10.1145\/3815107","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,7,15]]},"assertion":[{"value":"2023-03-13","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-03-31","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-07-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}