We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: HyperLTL Satisfiability is $Σ_1^1$-complete, HyperCTL* Satisfiability is $Σ_1^2$-complete

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.
Subjects: Logic in Computer Science (cs.LO)
MSC classes: 03D35
ACM classes: F.4.1; F.3.1
Cite as: arXiv:2105.04176 [cs.LO]
  (or arXiv:2105.04176v1 [cs.LO] for this version)

Submission history

From: Patrick Totzke [view email]
[v1] Mon, 10 May 2021 08:09:46 GMT (56kb,D)

Link back to: arXiv, form interface, contact.