Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Complexity of HyperQPTL

Gaëtan Regaud, Martin Zimmermann

TL;DR

This work resolves the exact complexities for HyperQPTL and HyperQPTL$^+$, showing HyperQPTL satisfiability is $\Sigma^2_1$-complete, while HyperQPTL$^+$ (including satisfiability, finite-state satisfiability, and model-checking) is equivalent to truth in third-order arithmetic. The key approach is proving that HyperQPTL$^+$ and Hyper^2LTL have the same expressive power, allowing transfer of known third-order arithmetic hardness results. The paper provides detailed reductions and translations, including arithmetic encodings and the construction of auxiliary formulas to encode sets of traces and operations, thereby situating these hyperlogics squarely in the higher undecidability regime. The results clarify the relative expressiveness and decidability landscapes of HyperQPTL and HyperQPTL$^+$, informing both theoretical understanding and practical verification considerations of hyperproperties.

Abstract

HyperQPTL and HyperQPTL$^+$ are expressive specification languages for hyperproperties, i.e., 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 $Σ^2_1$-complete, the latter are all equivalent to truth in third-order arithmetic, i.e., all four are very undecidable.

The Complexity of HyperQPTL

TL;DR

This work resolves the exact complexities for HyperQPTL and HyperQPTL, showing HyperQPTL satisfiability is -complete, while HyperQPTL (including satisfiability, finite-state satisfiability, and model-checking) is equivalent to truth in third-order arithmetic. The key approach is proving that HyperQPTL and Hyper^2LTL have the same expressive power, allowing transfer of known third-order arithmetic hardness results. The paper provides detailed reductions and translations, including arithmetic encodings and the construction of auxiliary formulas to encode sets of traces and operations, thereby situating these hyperlogics squarely in the higher undecidability regime. The results clarify the relative expressiveness and decidability landscapes of HyperQPTL and HyperQPTL, informing both theoretical understanding and practical verification considerations of hyperproperties.

Abstract

HyperQPTL and HyperQPTL are expressive specification languages for hyperproperties, i.e., 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.

Paper Structure

This paper contains 12 sections, 7 theorems, 11 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Words, Traces, and Transition Systems
  4. Arithmetic
  5. HyperQPTL
  6. Syntax and Semantics
  7. HyperQPTL Satisfiability
  8. HyperQPTL$^+$
  9. Syntax and Semantics
  10. Second-order HyperLTL
  11. HyperQPTL$^+$ "is" Second-order HyperLTL
  12. Conclusion

Key Result

Theorem 1

There is a satisfiable $\mathrm{Hyper\-QPTL}\xspace$ sentence that has only models of cardinality $\mathfrak{c}$.

Figures (1)

  • Figure 1: The arithmetical hierarchy, the analytical hierarchy, and beyond.

Theorems & Definitions (12)

  • Theorem 1
  • proof
  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Theorem 2
  • Lemma 3
  • proof
  • Lemma 4
  • ...and 2 more