# Pebble automaton

In computer science, a pebble automaton is an extension of tree walking automata which allows the automaton to use a finite amount of "pebbles", used for marking tree node[citation needed]. The result is a model stronger than ordinary tree walking automata, but still strictly weaker than branching automata.

## Definitions

A pebble automaton is a tree walking automaton with an additional finite set of fixed size containing pebbles, identified with ${\displaystyle \{1,2,\dots ,n\}}$. 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) pebble automata with n pebbles is denoted ${\displaystyle DPA_{n}}$ (resp. ${\displaystyle PA_{n}}$). We also define ${\displaystyle DPA=\bigcup _{n}DPA_{n}}$ and likewise ${\displaystyle PA=\bigcup _{n}PA_{n}}$.

## Properties

• there exists a language recognized by a pebble automaton with 1 pebble, but not by any tree walking automaton; this implies that either ${\displaystyle TWA\subsetneq DPA}$ or these classes are incomparable, which is an open problem
• ${\displaystyle PA\subsetneq REG}$, i.e. pebble automata are strictly weaker than branching automata
• it is not known whether ${\displaystyle DPA=PA}$, i.e. whether pebble automata can be determinized
• it is not known whether pebble automata are closed under complementation
• the pebble hierarchy is strict, for every n ${\displaystyle PA_{n}\subsetneq PA_{n+1}}$ and ${\displaystyle DPA_{n}\subsetneq DPA_{n+1}}$

## Automata and logic

Pebble automata admit an interesting logical characterization. Let ${\displaystyle FO+TC}$ denote the set of tree properties describable in transitive closure first-order logic, and ${\displaystyle FO+{\text{pos}}\,TC}$ 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 ${\displaystyle PA\subseteq FO+TC}$ and, in fact, ${\displaystyle PA=FO+{\text{pos}}\,TC}$ - the languages recognized by pebble automata are exactly those expressible in positive transitive closure logic.