First-Order Logic with Two Variables and Unary Temporal Logic
DOI:
https://doi.org/10.7146/brics.v4i5.18784Resumé
We investigate the power of first-order logic with only two variables overomega-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 FO3 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.
Downloads
Publiceret
1997-01-05
Citation/Eksport
Etessami, K., Vardi, M. Y., & Wilke, T. (1997). First-Order Logic with Two Variables and Unary Temporal Logic. BRICS Report Series, 4(5). https://doi.org/10.7146/brics.v4i5.18784
Nummer
Sektion
Artikler
Licens
Authors who publish with this journal agree to the following terms:- Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
- Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
- Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).