## 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} }