The complexity of HyperQPTL
HyperQPTL and HyperQPTL<sup>+</sup> 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<sup>+</sup>: the former is Σ<sub>1</sub><sup>2</sup>-complete, the latter are all equivalent to truth in third-order arithmetic, i.e., all four are very undecidable.
Authors
- Gaëtan Regaud (ORCID: https://orcid.org/0009-0000-1409-5707)
- Martin Zimmermann
Publication Details
- Journal
- Information Processing Letters
- Published
- 2026-02-17
- DOI
- https://doi.org/10.1016/j.ipl.2026.106626
- Primary Topic
- Formal Methods in Verification
- Type
- article
- Field-Weighted Citation Impact
- 0.00