First-Order Logic with Two Variables and Unary Temporal Logic

Kousha Etessami, Moshe Y. Vardi, Thomas Wilke

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

We investigate the power of first-order logic with only two variables over ω-words and finite words, a logic denoted by FO2. We prove that FO2 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 FO2 to unary-TL converts every FO2 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 FO2 is NEXP-complete, in sharp contrast to the fact that satisfiability for FO 3 has non-elementary computational complexity. Our NEXP time upper bound for FO2 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 FO2 of independent interest, namely: a satisfiable FO2 formula has a model whose “size” is at most exponential in the quantifier depth of the formula. Using our translation from FO2 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
Original languageEnglish
Title of host publicationProceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages8
ISBN (Print)0-8186-7925-5
Publication statusPublished - 1997


Dive into the research topics of 'First-Order Logic with Two Variables and Unary Temporal Logic'. Together they form a unique fingerprint.

Cite this