The Complexity of HyperQPTL

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 $\hat{I}{\pounds }_1^2$-complete, the latter are all equivalent to truth in third-order arithmetic, i.e., all four are very undecidable.

Updated with a fixed proof of Theorem 2, showing that HyperQPTL satisfiability is $\hat{I}{\pounds }_1^2$-complete