Paper: First-Order Logic with Two Variables and Unary Temporal Logic (at LICS 1997)

Authors: Kousha Etessami Moshe Y. Vardi Thomas Wilke

Abstract

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

BibTeX

  @InProceedings{EtessamiVardiWilke-FirstOrderLogicwith,
    author = 	 {Kousha Etessami and Moshe Y. Vardi and Thomas Wilke},
    title = 	 {First-Order Logic with Two Variables and Unary Temporal Logic},
    booktitle =  {Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS 1997)},
    year =	 {1997},
    month =	 {June}, 
    pages =      {228--235},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }