Paper: Ground Reducibility is EXPTIME-complete (at LICS 1997)

Authors: Hubert Comon-Lundh Florent Jacquemard

Abstract

We prove that ground reducibility is EXPTIME-complete in the general case EXPTIME-hardness is proved by encoding the computations of an alternating Turing machine whose space is polynomially bounded. It is more difficult to show the DEXPTIME-inclusion. Our algorithm first computes an automaton with disequality constraints, A, such that the term t is ground reducible w.r.t. R if and only if the language accepted by A is empty. The number of states of A is an exponential in the sizes of R and t and its constraints are polynomial in R, t. Then we introduce a new notion of pumping (relative to an ordering >) and show some properties of minimal computations of A. Finally we provide with an algorithm which decides the emptiness of the language accepted by A and whose complexity is bounded by a polynomial in |Q| (the number of states of the automaton) and an exponential in the size of its constraints. This yields the EXPTIME membership.

BibTeX

  @InProceedings{ComonLundhJacquemar-GroundReducibilityi,
    author = 	 {Hubert Comon-Lundh and Florent Jacquemard},
    title = 	 {Ground Reducibility is EXPTIME-complete},
    booktitle =  {Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS 1997)},
    year =	 {1997},
    month =	 {June}, 
    pages =      {26--34},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }