Logic in Computer Science (LICS 1997)

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

Authors: Hubert Comon 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{ComonJacquemard-GroundReducibilityi,
    author = 	 {Hubert Comon and Florent Jacquemard},
    title = 	 {Ground Reducibility is EXPTIME-complete},
    booktitle =  {Proceedings of the Twelfth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1997},
    year =	 1997,
    editor =	 {Glynn Winskel},
    month =	 {June}, 
    pages =      {26--34},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }