Complexity of Two-Variable Logic on Finite Trees

Verification of properties expressed in the two-variable fragment of first-order logic FO

2

has been investigated in a number of contexts. The satisfiability problem for FO

2

over arbitrary structures is known to be

NEXPTIME

-complete, with satisfiable formulas having exponential-sized models. Over words, where FO

2

is known to have the same expressiveness as unary temporal logic, satisfiability is again

NEXPTIME

-complete. Over finite labelled ordered trees FO

2

has the same expressiveness as navigational XPath, a popular query language for XML documents. Prior work on XPath and FO

2

gives a

2EXPTIME

bound for satisfiability of FO

2

over trees. This work contains a comprehensive analysis of the complexity of FO

2

on trees, and on the size and depth of models. We show that the exact complexity varies according to the vocabulary used, the presence or absence of a schema, and the encoding of labels on trees. We also look at a natural restriction of FO

2

, its guarded version, GF

2

. Our results depend on an analysis of types in models of FO

2

formulas, including techniques for controlling the number of distinct subtrees, the depth, and the size of a witness to satisfiability for FO

2

sentences over finite trees.