The Complexity of HyperQPTL

TL;DR

This paper establishes the high computational complexity and undecidability results for HyperQPTL and HyperQPTL$^+$, advanced logical languages for specifying hyperproperties involving multiple system executions.

Contribution

It determines the precise complexity and undecidability bounds for satisfiability and model-checking in HyperQPTL and HyperQPTL$^+$, resolving open questions.

Findings

HyperQPTL satisfiability is $ ext{Sigma}_1^2$-complete.

HyperQPTL$^+$ satisfiability and model-checking are equivalent to truth in third-order arithmetic.

All problems are highly undecidable.

Abstract

HyperQPTL and HyperQPTL$^+$ are expressive specification languages for hyperproperties, properties that relate multiple executions of a system. Tight complexity bounds are known for HyperQPTL finite-state satisfiability and model-checking. Here, we settle the complexity of satisfiability for HyperQPTL as well as satisfiability, finite-state satisfiability, and model-checking for HyperQPTL$^+$: the former is $\Sigma^2_1$-complete, the latter are all equivalent to truth in third-order arithmetic, i.e., all four are very undecidable.