CSL Conference 2024 Conference Paper
A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic
- Thomas Place
- Marc Zeitoun
We study an operator on classes of languages. For each class π, it produces a new class FOΒ²(π_π) associated with a variant of two-variable first-order logic equipped with a signature π_π built from π. For π = {β , A*}, we obtain the usual FOΒ²(<)} logic, equipped with linear order. For π = {β , {Ξ΅}, A+, A*}, we get the variant FOΒ²(<, +1), which also includes the successor predicate. If π consists of all Boolean combinations of languages A*aA*, where a is a letter, we get the variant FOΒ²(<, Bet), which includes "between" relations. We prove a generic algebraic characterization of the classes FO^2(π_π). It elegantly generalizes those known for all the cases mentioned above. Moreover, it implies that if π has decidable separation (plus some standard properties), then FOΒ²2(π_π) has a decidable membership problem. We actually work with an equivalent definition of FOΒ²(π_π) in terms of unary temporal logic. For each class π, we consider a variant TL(π) of unary temporal logic whose future/past modalities depend on π and such that TL(π) = FOΒ²(π_π). Finally, we also characterize FL(π) and PL(π), the pure-future and pure-past restrictions of TL(π). Like for TL(π), these characterizations imply that if π is a class with decidable separation, then FL(π) and PL(π) have decidable membership.