Pebble automaton

In computer science, a pebble automaton is any variant of an automaton which augments the original model with a finite number of "pebbles" that may be used to mark tape positions. 
History.
Pebble automata were introduced in 1986, when it was shown that in some cases, a deterministic transducer augmented with a pebble could achieve logarithmic space savings over even a nondeterministic log-space transducer (ie, compute in formula_1 tape cells functions for which the nondeterministic machine required formula_2 tape cells), with the implication that a pebble adds power to Turing machines whose functions require space between formula_3 and formula_4 Constructions were also shown to convert a hierarchy of increasingly powerful stack machine models into equivalent deterministic finite automata with up to 3 pebbles, showing additional pebbles further increased power.
Tree-walking automata with nested pebbles.
A tree-walking automaton with nested pebbles is a tree-walking automaton with an additional finite set of fixed size containing pebbles, identified with formula_5. Besides ordinary actions, an automaton can put a pebble at a currently visited node, lift a pebble from the currently visited node and perform a test "is the i-th pebble present at the current node?". There is an important stack restriction on the order in which pebbles can be put or lifted - the i+1-th pebble can be put only if the pebbles from 1st to i-th are already on the tree, and the i+1-th pebble can be lifted only if pebbles from i+2-th to n-th are not on the tree. Without this restriction, the automaton has undecidable emptiness and expressive power beyond regular tree languages.
The class of languages recognized by deterministic (resp. nondeterministic) tree-walking automata with n pebbles is denoted formula_6 (resp. formula_7). We also define formula_8 and likewise formula_9.
Automata and logic.
Tree-walking pebble automata admit an interesting logical characterization. Let formula_15 denote the set of tree properties describable in transitive closure first-order logic, and formula_16 the same for positive transitive closure logic, i.e. a logic where the transitive closure operator is not used under the scope of negation. Then it can be proved that formula_17 and, in fact, formula_18 - the languages recognized by tree-walking pebble automata are exactly those expressible in positive transitive closure logic.