Abstract:
We investigate the power of first-order logic with only two
variables over 
-words and finite words, a logic denoted by
. We prove that can express precisely the same
properties as linear temporal logic with only the unary temporal operators:
``next'', ``previously'', ``sometime in the future'', and ``sometime in the
past'', a logic we denote by unary-TL. Moreover, our translation from
to unary-TL converts every formula to an
equivalent unary-TL formula that is at most exponentially larger, and whose
operator depth is at most twice the quantifier depth of the first-order
formula. We show that this translation is optimal.
While
satisfiability for full linear temporal logic, as well as for unary-TL, is
known to be PSPACE-complete, we prove that satisfiability for
is NEXP-complete, in sharp contrast to the fact that satisfiability for
has non-elementary computational complexity. Our NEXP time
upper bound for satisfiability has the advantage of being in
terms of the quantifier depth of the input formula. It is obtained
using a small model property for of independent interest,
namely: a satisfiable formula has a model whose ``size'' is at
most exponential in the quantifier depth of the formula. Using our
translation from to unary-TL we derive this small model
property from a corresponding small model property for unary-TL. Our proof of
the small model property for unary-TL is based on an analysis of unary-TL
types
Available as PostScript, PDF, DVI.