The Complexity of HyperQPTL
Logic in Computer Science
2026-02-24 v3
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 -complete, the latter are all equivalent to truth in third-order arithmetic, i.e., all four are very undecidable.
Cite
@article{arxiv.2412.07341,
title = {The Complexity of HyperQPTL},
author = {Gaëtan Regaud and Martin Zimmermann},
journal= {arXiv preprint arXiv:2412.07341},
year = {2026}
}
Comments
Updated with a fixed proof of Theorem 2, showing that HyperQPTL satisfiability is $\Sigma_1^2$-complete