We use cookies on this website. Our privacy policy explains what cookies are and how they are being used here. If you continue to access our website, we'll assume that you consent to receiving cookies from this website.

Verification of properties of first order logic with two variables (FO^2) over words, where FO^2 is known to have the same expressiveness as unary temporal logic, is known to be decidable with NEXPTIME complexity, with finitely satisfiable formulas having exponential-sized models. Over finite labelled ordered trees FO^2 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 FO^2 gives a 2EXPTIME bound for satisfiability of FO^2. 

In this work we give the first in-depth look at the complexity of FO^2 on trees. We show that the 2EXPTIME bound is not tight, and neither do the NEXPTIME-completeness results from the word case carry over. Our results depend on an analysis of subformula types, including techniques for controlling the number of distinct subtrees, the depth, and the size of a witness to finite satisfiability for FO^2 sentences over trees.

This is joint work with Saguy Benaim, Michael Benedikt, and James Worrell