{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:20:50Z","timestamp":1776316850732,"version":"3.50.1"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"accepted":{"date-parts":[[2025,1,10]]},"abstract":"<jats:p>Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e. satisfiability is undecidable for both logics. In this paper we settle the exact complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL satisfiability is $\\Sigma_1^1$-complete and HyperCTL* satisfiability is $\\Sigma_1^2$-complete. These are significant increases over the previously known lower bounds and the first upper bounds. To prove $\\Sigma_1^2$-membership for HyperCTL*, we prove that every satisfiable HyperCTL* sentence has a model that is equinumerous to the continuum, the first upper bound of this kind. We also prove this bound to be tight. Furthermore, we prove that both countable and finitely-branching satisfiability for HyperCTL* are as hard as truth in second-order arithmetic, i.e. still highly undecidable. Finally, we show that the membership problem for every level of the HyperLTL quantifier alternation hierarchy is $\\Pi_1^1$-complete.<\/jats:p><jats:p>Comment: arXiv admin note: substantial text overlap with arXiv:2105.04176<\/jats:p>","DOI":"10.46298\/lmcs-21(1:3)2025","type":"journal-article","created":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T10:15:10Z","timestamp":1736504110000},"source":"Crossref","is-referenced-by-count":3,"title":["HyperLTL Satisfiability Is Highly Undecidable, HyperCTL$^*$ is Even Harder"],"prefix":"10.46298","volume":"Volume 21, Issue 1","author":[{"given":"Marie","family":"Fortin","sequence":"first","affiliation":[]},{"given":"Louwe B.","family":"Kuijer","sequence":"additional","affiliation":[]},{"given":"Patrick","family":"Totzke","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Zimmermann","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2025,1,10]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/15048\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/15048\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T10:15:10Z","timestamp":1736504110000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/11608"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,10]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-21(1:3)2025","relation":{"has-preprint":[{"id-type":"arxiv","id":"2303.16699v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2303.16699v2","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2303.16699","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2303.16699","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,10]]},"article-number":"11608"}}