  The pebble tree automaton and the pebble tree transducer are enhanced by
additionally allowing an unbounded number of "invisible" pebbles (as opposed to
the usual "visible" ones). The resulting pebble tree automata recognize the
regular tree languages (i.e., can validate all generalized DTD's) and hence can
find all matches of MSO definable patterns. Moreover, when viewed as a
navigational device, they lead to an XPath-like formalism that has a path
expression for every MSO definable binary pattern. The resulting pebble tree
transducers can apply arbitrary MSO definable tests to (the observable part of)
their configurations, they (still) have a decidable typechecking problem, and
they can model the recursion mechanism of XSLT. The time complexity of the
typechecking problem for conjunctive queries that use MSO definable patterns
can often be reduced through the use of invisible pebbles.
