Fortin, Marie, Kuijer, Louwe B, Totzke, Patrick 
ORCID: 0000-0001-5274-8190 and Zimmermann, Martin
(2021)
HyperLTL Satisfiability is $Σ_1^1$-complete, HyperCTL*
Satisfiability is $Σ_1^2$-complete.
Leibniz International Proceedings in Informatics, LIPIcs, 202.
|
Text
2105.04176v1.pdf - Submitted version Download (766kB) | Preview |
Abstract
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 prove this bound to be tight. Finally, we show that the membership problem for every level of the HyperLTL quantifier alternation hierarchy is $\Pi_1^1$-complete.
| Item Type: | Article |
|---|---|
| Uncontrolled Keywords: | cs.LO, cs.LO, 03D35, F.4.1; F.3.1 |
| Divisions: | Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 15 Jul 2021 08:04 |
| Last Modified: | 18 Jan 2023 21:35 |
| DOI: | 10.4230/LIPIcs.MFCS.2021.47 |
| Open Access URL: | https://drops.dagstuhl.de/opus/volltexte/2021/1448... |
| Related URLs: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3130034 |
Dimensions
Dimensions
