Tree-Walking Pebble Automata

The tree languages accepted by (finite state) tree-walking automata are known to form a subclass of the regular tree languages which is not known to be proper. They include all locally first-order definable tree languages. We allow the tree-walking automaton to use a finite number of pebbles, which have to be dropped and lifted in a nested fashion. The class of tree languages accepted by these tree-walking pebble automata contains all first-order definable tree languages and is still included in the class of regular tree languages. It also contains all deterministic top-down recognizable tree languages.