English

A generic characterization of generalized unary temporal logic and two-variable first-order logic

Formal Languages and Automata Theory 2023-11-30 v2 Logic in Computer Science

Abstract

We investigate an operator on classes of languages. For each class CC, it outputs a new class FO2(IC)FO^2(I_C) associated with a variant of two-variable first-order logic equipped with a signatureICI_C built from CC. For C={,A}C = \{\emptyset, A^*\}, we get the variant FO2(<)FO^2(<) equipped with the linear order. For C={,{ε},A+,A}C = \{\emptyset, \{\varepsilon\},A^+, A^*\}, we get the variant FO2(<,+1)FO^2(<,+1), which also includes the successor. If CC consists of all Boolean combinations of languages AaAA^*aA^* where aa is a letter, we get the variant FO2(<,Bet)FO^2(<,Bet), which also includes "between relations". We prove a generic algebraic characterization of the classes FO2(IC)FO^2(I_C). It smoothly and elegantly generalizes the known ones for all aforementioned cases. Moreover, it implies that if CC has decidable separation (plus mild properties), then FO2(IC)FO^2(I_C) has a decidable membership problem. We actually work with an equivalent definition of \fodc in terms of unary temporal logic. For each class CC, we consider a variant TL(C)TL(C) of unary temporal logic whose future/past modalities depend on CC and such that TL(C)=FO2(IC)TL(C) = FO^2(I_C). Finally, we also characterize FL(C)FL(C) and PL(C)PL(C), the pure-future and pure-past restrictions of TL(C)TL(C). These characterizations as well imply that if \Cs is a class with decidable separation, then FL(C)FL(C) and PL(C)PL(C) have decidable membership.

Keywords

Cite

@article{arxiv.2307.09349,
  title  = {A generic characterization of generalized unary temporal logic and two-variable first-order logic},
  author = {Thomas Place and Marc Zeitoun},
  journal= {arXiv preprint arXiv:2307.09349},
  year   = {2023}
}

Comments

Extended version of CLS 2024 paper

R2 v1 2026-06-28T11:33:42.592Z