HyperLTL Satisfiability Is Highly Undecidable, HyperCTL\(^\) is Even Harder

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...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2024-12
Main Authors: tin, Marie, Kuijer, Louwe B, Totzke, Patrick, Zimmermann, Martin
Format: Article
Language:English
Subjects:
Information flow
Lower bounds
Upper bounds
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422