دورية أكاديمية
A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic
العنوان: | A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic |
---|---|
المؤلفون: | Place, Thomas, Zeitoun, Marc |
المساهمون: | Thomas Place and Marc Zeitoun |
بيانات النشر: | Schloss Dagstuhl – Leibniz-Zentrum für Informatik |
سنة النشر: | 2024 |
المجموعة: | DROPS - Dagstuhl Research Online Publication Server (Schloss Dagstuhl - Leibniz Center for Informatics ) |
مصطلحات موضوعية: | 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. |
نوع الوثيقة: | article in journal/newspaper conference object |
وصف الملف: | application/pdf |
اللغة: | English |
العلاقة: | Is Part Of LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024); urn:nbn:de:0030-drops-196888; https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.45Test |
DOI: | 10.4230/LIPIcs.CSL.2024.45 |
الإتاحة: | https://doi.org/10.4230/LIPIcs.CSL.2024.45Test https://nbn-resolving.org/urn:nbn:de:0030-drops-196888Test |
حقوق: | https://creativecommons.org/licenses/by/4.0/legalcodeTest |
رقم الانضمام: | edsbas.E185FDAE |
قاعدة البيانات: | BASE |
DOI: | 10.4230/LIPIcs.CSL.2024.45 |
---|