2026-08-07T03:51:28Z https://drops.dagstuhl.de/oai
oai:drops-oai.dagstuhl.de:19688 2024-03-06T11:04:39Z ddc:004 open_access
A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic Place, Thomas Zeitoun, Marc Classes of regular languages Generalized unary temporal logic Generalized two-variable first-order logic Generic decidable characterizations Membership Separation 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. Schloss Dagstuhl – Leibniz-Zentrum fΓΌr Informatik Thomas Place and Marc Zeitoun 2024 Is Part Of LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2024.45 urn:nbn:de:0030-drops-196888 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.45 eng https://creativecommons.org/licenses/by/4.0/legalcode