HyperLTL Satisfiability Is Highly Undecidable, HyperCTL$^*$ is Even Harder

TL;DR

This work resolves the exact complexity of satisfiability for the hyperproperty logics HyperLTL and HyperCTL*, placing HyperLTL satisfiability at $\Sigma_1^1$-complete and HyperCTL* satisfiability at $\Sigma_1^2$-complete. It introduces a tight continuum-model bound for satisfiable HyperCTL* formulas and shows this bound is tight, with the same bound holding for countable and finitely-branching cases, which remain highly undecidable. The authors also establish that HyperLTL quantifier-alternation membership is $\Pi_1^1$-complete, and they prove the HyperLTL/HyperCTL* results by combining model-theoretic constructions (countable/continuum Skolem models) with reductions from arithmetic hierarchies. Overall, the paper maps the full undecidability landscape for these logics, clarifying both upper and lower bounds and the impact of model size on complexity.

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 $Σ_1^1$-complete and HyperCTL* satisfiability is $Σ_1^2$-complete. These are significant increases over the previously known lower bounds and the first upper bounds. To prove $Σ_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 $Π_1^1$-complete.

Figures (3)

• Figure 1: Example of a split set of traces where each row represents a trace and $b=3$.
• Figure 2: A depiction of $\mathcal{T}_{\mathfrak{c}}$. Vertices in black (on the left including the initial vertex) are labelled by $\textup{fbt}$, those in red (on the right, excluding the initial vertex) are labelled by $\textup{set}$.
• Figure 3: A depiction of $\mathcal{T}_f$. All vertices but the initial one are labelled by $\textup{fbt}$.

Theorems & Definitions (59)

• Theorem 3.1
• Lemma 3.2
• proof
• Lemma 3.3
• proof
• Theorem 3.4
• proof
• Proposition 3.5: FinkbeinerRS15FinkbeinerH16
• Theorem 4.1: Rabe16
• Theorem 4.2