It is known that a sentence of first-order logic of quantifier rank k can only express reachability in a directed graph of diameter at most 2^k. Thus, general directed graph reachability is not expressible in first-order logic. The author of this paper considers the formalism of two-way alternating automata with k pebbles over an infinite alphabet, which is more expressive than first-order logic over an appropriate signature.

Tan proves a similar bound for this model, showing that general directed graph reachability cannot be modeled using pebble automata. The paper also establishes a strict hierarchy depending on the number of pebbles. A hierarchy of pebble automata on binary trees is considered in an earlier paper [1], but Tan does not refer to it.