Automatic structures of bounded degree revisited

TL;DR

This paper proves that the first-order theory of string and tree automatic structures with bounded degree is decidable in doubly exponential space, establishing optimal bounds and extending previous results in the field.

Contribution

It establishes the decidability and complexity bounds for the first-order theory of bounded degree automatic structures, improving previous bounds and including tree structures.

Findings

Decidability of first-order theory in doubly exponential space for bounded degree structures

Existence of a bounded degree automatic structure with a 2EXPSPACE-hard first-order theory

Extension of results to both string and tree automatic structures

Abstract

The first-order theory of a string automatic structure is known to be decidable, but there are examples of string automatic structures with nonelementary first-order theories. We prove that the first-order theory of a string automatic structure of bounded degree is decidable in doubly exponential space (for injective automatic presentations, this holds even uniformly). This result is shown to be optimal since we also present a string automatic structure of bounded degree whose first-order theory is hard for 2EXPSPACE. We prove similar results also for tree automatic structures. These findings close the gaps left open in a previous paper of the second author by improving both, the lower and the upper bounds.