How undecidable are HyperLTL and HyperCTL*?

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. We settle the exact complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL is satisfiability complete for and HyperCTL* satisfiability is complete for. These are significant increases over the previously known lower bounds and the first upper bounds. To prove membership for HyperCTL*, we prove that every satisfiable HyperCTL* formula 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 -complete. This is joint work with Louwe B. Kuijer, Patrick Totzke and Martin Zimmermann.

Authors

• Marie Fortin

Keywords

No keywords are indexed for this paper.