  Verification of properties of first order logic with two variables FO2 has
been investigated in a number of contexts. Over arbitrary structures it is
known to be decidable with NEXPTIME complexity, with finitely satisfiable
formulas having exponential-sized models. Over word structures, where FO2 is
known to have the same expressiveness as unary temporal logic, the same
properties hold. Over finite labelled ordered trees FO2 is also of interest: it
is known to have the same expressiveness as navigational XPath, a common query
language for XML documents. Prior work on XPath and FO2 gives a 2EXPTIME bound
for satisfiability of FO2. In this work we give the first in-depth look at the
complexity of FO2 on trees, and on the size and depth of models. We show that
the doubly-exponential bound is not tight, and neither do the
NEXPTIME-completeness results from the word case carry over: the exact
complexity varies depending on the vocabulary used, the presence or absence of
a schema, and the encoding used for labels. Our results depend on an analysis
of subformula types in models of FO2 formulas, including techniques for
controlling the number of distinct subtrees, the depth, and the size of a
witness to finite satisfiability for FO2 sentences over trees.
