Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Complexity of Generalized HyperLTL with Stuttering and Contexts

Gaëtan Regaud, Martin Zimmermann

TL;DR

The paper addresses complexity for the asynchronous hyperproperty logic GHyLTL_S+C, focusing on satisfiability, finite-state satisfiability, and model-checking. It proves satisfiability is $Σ_1^1$-complete (not harder than Hyper-LTL), while both model-checking and finite-state satisfiability are equivalent to truth in second-order arithmetic, a significantly higher complexity. A key contribution is a small-model property: every satisfiable formula has a countable model, enabling arithmetic encodings and Skolem-function constructions to establish the upper bounds. The results hold for important fragments like HyperLTL_S and HyperLTL_C and clarify the computational landscape relative to HyperCTL^*$, with implications for verification of asynchronous hyperproperties and future work on other asynchronous logics.

Abstract

We settle the complexity of satisfiability, finite-state satisfiability, and model-checking for generalized HyperLTL with stuttering and contexts, an expressive logic for the specification of asynchronous hyperproperties. Such properties cannot be specified in HyperLTL, as it is restricted to synchronous hyperproperties. Nevertheless, we prove that satisfiability is $Σ_1^1$-complete and thus not harder than for HyperLTL. On the other hand, we prove that model-checking and finite-state satisfiability are equivalent to truth in second-order arithmetic, and thus much harder than the decidable HyperLTL model-checking problem and the $Σ_0^1$-complete HyperLTL finite-state satisfiability problem. The lower bounds for the model-checking and finite-state satisfiability problems hold even when only allowing stuttering or only allowing contexts.

The Complexity of Generalized HyperLTL with Stuttering and Contexts

TL;DR

The paper addresses complexity for the asynchronous hyperproperty logic GHyLTL_S+C, focusing on satisfiability, finite-state satisfiability, and model-checking. It proves satisfiability is -complete (not harder than Hyper-LTL), while both model-checking and finite-state satisfiability are equivalent to truth in second-order arithmetic, a significantly higher complexity. A key contribution is a small-model property: every satisfiable formula has a countable model, enabling arithmetic encodings and Skolem-function constructions to establish the upper bounds. The results hold for important fragments like HyperLTL_S and HyperLTL_C and clarify the computational landscape relative to HyperCTL^*$, with implications for verification of asynchronous hyperproperties and future work on other asynchronous logics.

Abstract

We settle the complexity of satisfiability, finite-state satisfiability, and model-checking for generalized HyperLTL with stuttering and contexts, an expressive logic for the specification of asynchronous hyperproperties. Such properties cannot be specified in HyperLTL, as it is restricted to synchronous hyperproperties. Nevertheless, we prove that satisfiability is -complete and thus not harder than for HyperLTL. On the other hand, we prove that model-checking and finite-state satisfiability are equivalent to truth in second-order arithmetic, and thus much harder than the decidable HyperLTL model-checking problem and the -complete HyperLTL finite-state satisfiability problem. The lower bounds for the model-checking and finite-state satisfiability problems hold even when only allowing stuttering or only allowing contexts.

Paper Structure

This paper contains 11 sections, 13 theorems, 27 equations, 6 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. LTL with Past
  4. Stuttering
  5. Generalized HyperLTL with Stuttering and Contexts
  6. Arithmetic and Complexity Classes for Undecidable Problems
  7. "Small" Models for Generalized HyperLTL with Stuttering and Contexts
  8. Generalized HyperLTL with Stuttering and Contexts Satisfiability
  9. Model-Checking Generalized HyperLTL with Stuttering and Contexts
  10. Generalized HyperLTL with Stuttering and Contexts Finite-state Satisfiability
  11. Conclusion

Key Result

Lemma 3.1

Let $\mathrm{AP}$ be a finite set of propositions and $\texttt{\#}\not\in\mathrm{AP}$. For every GHyLTL$_\textrm{S+C}$ sentence $\varphi$ over $\mathrm{AP}$, there exists a polynomial-time computable GHyLTL$_\textrm{S+C}$ sentence $\varphi_p$ in prenex normal form over $\mathrm{AP}\cup \{\texttt{\#}

Figures (6)

  • Figure 1: The landscape of logics for asynchronous hyperproperties. Arrows denote known inclusions and the dashed line denotes the decidability border for model-checking. For non-inclusions, we refer the reader to work by Bozelli et al. expressivenessDBLP:conf/fsttcs/BombardelliB0T24.
  • Figure 2: The arithmetical hierarchy, the analytical hierarchy, and beyond.
  • Figure 3: The formula $\alpha_\mathrm{add}$ implements addition, illustrated here for $n_1 = 5$ and $n_2 = 4$.
  • Figure 4: The formula $\alpha_3$ ensures that the traces assigned to $x$ and $x'$ are periodic. Here, " " denotes a position where $\$$ ($\$'$) holds and " " a position where $\$$ ($\$'$) does not hold.
  • Figure 5: The formula $\alpha_3$ ensures that the traces assigned to $x$ (and $x'$) are periodic. Here, " " (" ") denotes a position where $\$$ holds (does not hold).
  • ...and 1 more figures

Theorems & Definitions (26)

  • Remark 2.1
  • Remark 2.2
  • Lemma 3.1
  • proof
  • Lemma 3.2
  • proof
  • Theorem 3.3
  • Theorem 4.1
  • proof
  • Corollary 4.2
  • ...and 16 more