Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Characterizing the Exponential-Space Hierarchy Via Partial Fixpoints

Florian Bruse, David Kronenberger, Martin Lange

TL;DR

The paper addresses the descriptive-complexity question of characterizing k-EXPSPACE queries via logic. It extends Vardi's PSPACE result by showing that HO^{k+1}+PFP captures k-EXPSPACE over LTS, with order requirements eliminable when k ≥ 1, and it mirrors Freire-Martins' approach for the EXPTIME hierarchy. The authors provide explicit encodings of space-bounded computations into higher-order partial fixpoints, including detailed constructions of initialization, transition, and fixpoint formulas, and prove both directions of the capture. This establishes a tight correspondence between exponential-space resources and high-order logical definability, enabling precise reasoning about the exponential-space hierarchy and its potential bisimulation-invariant extensions.

Abstract

The characterization of PSPACE-queries over ordered structures as exactly those expressible in first-order logic with partial fixpoints (Vardi'82) is one of the classical results in the field of descriptive complexity. In this paper, we extend this result to characterizations of k-EXPSPACE-queries for arbitrary k, characterizing them as exactly those expressible in order-k+1-higher-order logic with partial fixpoints. For k>1, the restriction to ordered structures is no longer necessary due to the high expressive power of higher-order logic.

Characterizing the Exponential-Space Hierarchy Via Partial Fixpoints

TL;DR

The paper addresses the descriptive-complexity question of characterizing k-EXPSPACE queries via logic. It extends Vardi's PSPACE result by showing that HO^{k+1}+PFP captures k-EXPSPACE over LTS, with order requirements eliminable when k ≥ 1, and it mirrors Freire-Martins' approach for the EXPTIME hierarchy. The authors provide explicit encodings of space-bounded computations into higher-order partial fixpoints, including detailed constructions of initialization, transition, and fixpoint formulas, and prove both directions of the capture. This establishes a tight correspondence between exponential-space resources and high-order logical definability, enabling precise reasoning about the exponential-space hierarchy and its potential bisimulation-invariant extensions.

Abstract

The characterization of PSPACE-queries over ordered structures as exactly those expressible in first-order logic with partial fixpoints (Vardi'82) is one of the classical results in the field of descriptive complexity. In this paper, we extend this result to characterizations of k-EXPSPACE-queries for arbitrary k, characterizing them as exactly those expressible in order-k+1-higher-order logic with partial fixpoints. For k>1, the restriction to ordered structures is no longer necessary due to the high expressive power of higher-order logic.

Paper Structure

This paper contains 11 sections, 6 theorems, 15 equations, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Space-bounded Turing Machines
  4. Higher-Order Logic with Partial Fixpoints
  5. Queries
  6. Vardi's Characterization of PSPACE
  7. HO-k+PFP-Queries are in k-1-EXPSPACE
  8. k-1-EXPSPACE-Queries are Expressible in HO-k+PFP
  9. Ordering Higher-Order Relations
  10. The Reduction
  11. Conclusion

Key Result

Lemma 1

For any $\tau$ of order $k$ and any LTS ${T}$, with state set ${S}$, $|\llbracket \tau \rrbracket^{{T}}_{}|$ is $k-1$-fold exponential in $|{S}|$.

Theorems & Definitions (9)

  • Lemma 1
  • Remark 2
  • Theorem 3
  • proof
  • Lemma 4
  • Definition 5
  • Lemma 6
  • Lemma 7
  • Theorem 8