{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,14]],"date-time":"2026-07-14T04:06:36Z","timestamp":1784001996864,"version":"3.55.0"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T00:00:00Z","timestamp":1779753600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T00:00:00Z","timestamp":1779753600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100007797","name":"University of Helsinki","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100007797","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2026,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Linear temporal logic (LTL) is used in system verification to write formal specifications for reactive systems. However, some relevant properties, e.g. non-inference in information flow security, cannot be expressed in LTL. A class of such properties that has recently received ample attention is known as hyperproperties. There are two major streams in the research regarding capturing hyperproperties, namely hyperlogics, which extend LTL with trace quantifiers (HyperLTL), and logics that employ team semantics, extending truth to sets of traces. In this article we explore the relation between asynchronous LTL under set-based team semantics (TeamLTL) and HyperLTL. In particular we consider the extensions of TeamLTL with the Boolean disjunction and a fragment of the extension of TeamLTL with the Boolean negation, where the negation cannot occur in the right-hand side of the strong release operator or within the global operator. We show that TeamLTL extended with the Boolean disjunction is equi-expressive with the positive Boolean closure of HyperLTL restricted to one universal quantifier, while the right-downward closed fragment of TeamLTL extended with the Boolean negation is expressively equivalent with the Boolean closure of HyperLTL restricted to one universal quantifier. Furthermore, we show that formulae of TeamLTL extended with the Boolean negation are equivalent with sentences of first-order logic interpreted over grid structures.<\/jats:p>","DOI":"10.1007\/s00236-025-00514-x","type":"journal-article","created":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T10:59:16Z","timestamp":1779793156000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Expressivity of asynchronous TeamLTL and HyperLTL"],"prefix":"10.1007","volume":"63","author":[{"given":"Juha","family":"Kontinen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Max","family":"Sandstr\u00f6m","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jonni","family":"Virtema","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,26]]},"reference":[{"key":"514_CR1","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"6","key":"514_CR2","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. Journal of Computer Security 18(6), 1157\u20131210 (2010)","journal-title":"Journal of Computer Security"},{"key":"514_CR3","doi-asserted-by":"publisher","unstructured":"Roscoe, A.W.: CSP and determinism in security modelling. In: Proceedings of the 1995 IEEE Symposium on Security and Privacy, Oakland, California, USA, May 8\u201310, 1995, pp. 114\u2013127. IEEE Computer Society (1995). https:\/\/doi.org\/10.1109\/SECPRI.1995.398927","DOI":"10.1109\/SECPRI.1995.398927"},{"issue":"1","key":"514_CR4","doi-asserted-by":"publisher","first-page":"37","DOI":"10.3233\/JCS-1992-1103","volume":"1","author":"J McLean","year":"1992","unstructured":"McLean, J.: Proving noninterference and functional correctness using traces. J. Comput. Secur. 1(1), 37\u201358 (1992). https:\/\/doi.org\/10.3233\/JCS-1992-1103","journal-title":"J. Comput. Secur."},{"key":"514_CR5","doi-asserted-by":"publisher","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: 16th IEEE Computer Security Foundations Workshop (CSFW-16 2003), 30 June\u20132 July 2003, Pacific Grove, CA, USA, p. 29. IEEE Computer Society (2003). https:\/\/doi.org\/10.1109\/CSFW.2003.1212703","DOI":"10.1109\/CSFW.2003.1212703"},{"issue":"1\u20132","key":"514_CR6","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/s00236-019-00358-2","volume":"57","author":"B Finkbeiner","year":"2020","unstructured":"Finkbeiner, B., Hahn, C., Lukert, P., Stenger, M., Tentrup, L.: Synthesis from hyperproperties. Acta Inform 57(1\u20132), 137\u2013163 (2020). https:\/\/doi.org\/10.1007\/s00236-019-00358-2","journal-title":"Acta Inform"},{"key":"514_CR7","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: POST 2014, pp. 265\u2013284 (2014)","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"514_CR8","unstructured":"Rabe, M.N.: A temporal logic approach to information-flow control. Ph.D. thesis, Saarland University (2016)"},{"key":"514_CR9","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., Hahn, C., Hofmann, J.: The hierarchy of hyperlogics. In: 34th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC Canada, June 24-27, 2019. IEEE, pp 1-13. IEEE (2019) https:\/\/doi.org\/10.1109\/LICS.2019.8785713","DOI":"10.1109\/LICS.2019.8785713"},{"key":"514_CR10","unstructured":"Krebs, A., Meier, A., Virtema, J., Zimmermann, M.: Team semantics for the specification and verification of hyperproperties. In: Potapov, I., Spirakis, P., Worrell, J. (eds.) MFCS 2018, vol. 117, pp. 10\u201311016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2018)"},{"key":"514_CR11","doi-asserted-by":"publisher","unstructured":"Gutsfeld, J.O., Meier, A., Ohrem, C., Virtema, J.: Temporal team semantics revisited. In: Baier, C., Fisman, D. (eds.) LICS \u201922: 37th Annual ACM\/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2\u20135, 2022, pp. 44\u201314413. ACM (2022). https:\/\/doi.org\/10.1145\/3531130.3533360","DOI":"10.1145\/3531130.3533360"},{"key":"514_CR12","doi-asserted-by":"publisher","unstructured":"Krebs, A., Meier, A., Virtema, J.: A team based variant of CTL. In: Grandi, F., Lange, M., Lomuscio, A. (eds.) 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015, Kassel, Germany, September 23\u201325, 2015, pp. 140\u2013149. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/TIME.2015.11","DOI":"10.1109\/TIME.2015.11"},{"key":"514_CR13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511611193","volume-title":"Dependence Logic","author":"J V\u00e4\u00e4n\u00e4nen","year":"2007","unstructured":"V\u00e4\u00e4n\u00e4nen, J.: Dependence Logic. Cambridge University Press (2007)"},{"key":"514_CR14","doi-asserted-by":"publisher","unstructured":"Virtema, J., Hofmann, J., Finkbeiner, B., Kontinen, J., Yang, F.: Linear-time temporal logic with team semantics: Expressivity and complexity. In: Bojanczyk, M., Chekuri, C. (eds.) 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021, December 15\u201317, 2021, Virtual Conference. LIPIcs, vol. 213, pp. 52\u201315217. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2021.52","DOI":"10.4230\/LIPIcs.FSTTCS.2021.52"},{"key":"514_CR15","doi-asserted-by":"crossref","unstructured":"Kontinen, J., Sandstr\u00f6m, M.: On the expressive power of teamltl and first-order team logic over hyperproperties. In: WoLLIC. Lecture Notes in Computer Science, vol. 13038, pp. 302\u2013318. Springer (2021)","DOI":"10.1007\/978-3-030-88853-4_19"},{"issue":"POPL","key":"514_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3434319","volume":"5","author":"JO Gutsfeld","year":"2021","unstructured":"Gutsfeld, J.O., M\u00fcller-Olm, M., Ohrem, C.: Automata and fixpoints for asynchronous hyperproperties. Proc. ACM Program. Lang. 5(POPL), 1\u201329 (2021). https:\/\/doi.org\/10.1145\/3434319","journal-title":"Proc. ACM Program. Lang."},{"key":"514_CR17","doi-asserted-by":"crossref","unstructured":"Baumeister, J., Coenen, N., Bonakdarpour, B., Finkbeiner, B., S\u00e1nchez, C.: A temporal logic for asynchronous hyperproperties. In: CAV (1). Lecture Notes in Computer Science, vol. 12759, pp. 694\u2013717. Springer (2021)","DOI":"10.1007\/978-3-030-81685-8_33"},{"key":"514_CR18","unstructured":"Finkbeiner, B., Zimmermann, M.: The first-order logic of hyperproperties. In: Vollmer, H., Vall\u00e9e, B. (eds.) STACS 2017. LIPIcs, vol. 66, pp. 30\u201313014. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017)"},{"key":"514_CR19","doi-asserted-by":"publisher","unstructured":"Kontinen, J., Sandstr\u00f6m, M., Virtema, J.: Set semantics for asynchronousteamltl: e xpressivity and complexity. Inf. Comput. 304, 105299 (2025) https:\/\/doi.org\/10.1016\/j.ic.2025.105299","DOI":"10.1016\/j.ic.2025.105299"},{"key":"514_CR20","doi-asserted-by":"publisher","unstructured":"Kontinen, J., Sandstr\u00f6m, M., Virtema, J.: A remark on the expressivity of asynchronous teamltl and hyperltl. In: Meier, A., Ortiz, M. (eds.) Foundations of Information and Knowledge Systems\u201413th International Symposium, FoIKS 2024, Sheffield, UK, April 8\u201311, 2024, Proceedings. Lecture Notes in Computer Science, vol. 14589, pp. 275\u2013286. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-56940-1_15","DOI":"10.1007\/978-3-031-56940-1_15"},{"key":"514_CR21","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B.: Temporal hyperproperties. Bull. EATCS 123 (2017)","DOI":"10.1007\/978-3-319-67531-2_12"},{"key":"514_CR22","doi-asserted-by":"publisher","unstructured":"Galliani, P.: On strongly first-order dependencies. In: Abramsky, S., Kontinen, J., V\u00e4\u00e4n\u00e4nen, J., Vollmer, H. (eds.) Dependence Logic, Theory and Applications, pp. 53\u201371. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-31803-5_4","DOI":"10.1007\/978-3-319-31803-5_4"},{"key":"514_CR23","unstructured":"L\u00fcck, M.: Team logic: axioms, expressiveness, complexity. Ph.D. thesis, University of Hanover, Hannover, Germany (2020). https:\/\/www.repo.uni-hannover.de\/handle\/123456789\/9430"},{"key":"514_CR24","doi-asserted-by":"publisher","unstructured":"Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Abrahams, P.W., Lipton, R.J., Bourne, S.R. (eds.) Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada, USA, January 1980, pp. 163\u2013173. ACM Press (1980). https:\/\/doi.org\/10.1145\/567446.567462","DOI":"10.1145\/567446.567462"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00514-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-025-00514-x","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00514-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,14]],"date-time":"2026-07-14T03:46:47Z","timestamp":1784000807000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-025-00514-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,5,26]]},"references-count":24,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,6]]}},"alternative-id":["514"],"URL":"https:\/\/doi.org\/10.1007\/s00236-025-00514-x","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,5,26]]},"assertion":[{"value":"30 November 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 July 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 May 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no Conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"18"}}