First-Order Logic with Two Variables and Unary Temporal Logic

Kousha Etessami
Moshe Y. Vardi
Thomas Wilke

March 1997


We investigate the power of first-order logic with only two variables over tex2html_wrap_inline31-words and finite words, a logic denoted by tex2html_wrap_inline33. We prove that tex2html_wrap_inline33 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 tex2html_wrap_inline33 to unary-TL converts every tex2html_wrap_inline33 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 tex2html_wrap_inline33 is NEXP-complete, in sharp contrast to the fact that satisfiability for tex2html_wrap_inline43 has non-elementary computational complexity. Our NEXP time upper bound for tex2html_wrap_inline33 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 tex2html_wrap_inline33 of independent interest, namely: a satisfiable tex2html_wrap_inline33 formula has a model whose ``size'' is at most exponential in the quantifier depth of the formula. Using our translation from tex2html_wrap_inline33 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.


Last modified: 2003-06-08 by webmaster.