First-Order Logic with Two Variables and Unary Temporal Logic
Kousha Etessami March 1997 |

## 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
Available as |

Last modified: 2003-06-08 by webmaster.