Automata with Nested Pebbles Capture First-Order Logic with Transitive Closure

摘要

String languages recognizable in (deterministic) log-space are characterizedeither by two-way (deterministic) multi-head automata, or following Immerman,by first-order logic with (deterministic) transitive closure. Here we elaboratethis result, and match the number of heads to the arity of the transitiveclosure. More precisely, first-order logic with k-ary deterministictransitive closure has the same power as deterministic automata walking ontheir input with k heads, additionally using a finite set of nestedpebbles. This result is valid for strings, ordered trees, and in general forfamilies of graphs having a fixed automaton that can be used to traverse thenodes of each of the graphs in the family. Other examples of such families aregrids, toruses, and rectangular mazes. For nondeterministic automata, the logicis restricted to positive occurrences of transitive closure. The special case of k=1 for trees, shows that single-headdeterministic tree-walking automata with nested pebbles are characterized byfirst-order logic with unary deterministic transitive closure. This refines ourearlier result that placed these automata between first-order and monadicsecond-order logic on trees.