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

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