2023/07/18 by Place, Thomas, Zeitoun, Marc
#FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2307.09349
We investigate an operator on classes of languages. For each class C, it outputs a new class FO2(IC) associated with a variant of two-variable first-order logic equipped with a signatureIC built from C. For C = \∅, A^*\, we get the variant FO2(<) equipped with the linear order. For C = \∅, \ε\,A+, A^*\, we get the variant FO2(<,+1), which also includes the successor. If C consists of all Boolean combinations of languages A^*aA^* where a is a letter, we get the variant FO2(<,Bet), which also includes "between relations". We prove a generic algebraic characterization of the classes FO2(IC). It smoothly and elegantly generalizes the known ones for all aforementioned cases. Moreover, it implies that if C has decidable separation (plus mild properties), then FO2(IC) has a decidable membership problem. We actually work with an equivalent definition of \fodc in terms of unary temporal logic. For each class C, we consider a variant TL(C) of unary temporal logic whose future/past modalities depend on C and such that TL(C) = FO2(IC). Finally, we also characterize FL(C) and PL(C), the pure-future and pure-past restrictions of TL(C). These characterizations as well imply that if \Cs is a class with decidable separation, then FL(C) and PL(C) have decidable membership.