Document Open Access Logo

A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic

Authors Thomas Place , Marc Zeitoun

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2024.45.pdf
  • Filesize: 0.87 MB
  • 23 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Classes of regular languages
  • Generalized unary temporal logic
  • Generalized two-variable first-order logic
  • Generic decidable characterizations
  • Membership
  • Separation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get BibTex

Thomas Place and Marc Zeitoun. A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 45:1-45:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CSL.2024.45

Author Details

Thomas Place
  • Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400, Talence, France
Marc Zeitoun
  • Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400, Talence, France

References

  1. Mustapha Arfi. Polynomial operations on rational languages. In Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science, STACS'87, Lecture Notes in Computer Science, pages 198-206. Springer, 1987. Google Scholar
  2. David A. Mix Barrington, Kevin Compton, Howard Straubing, and Denis Thérien. Regular languages in NC¹. Journal of Computer and System Sciences, 44(3):478-499, 1992. Google Scholar
  3. Danièle Beauquier and Jean-Éric Pin. Languages and scanners. Theoretical Computer Science, 84(1):3-21, 1991. Google Scholar
  4. Janusz A. Brzozowski and Imre Simon. Characterizations of locally testable events. Discrete Mathematics, 4(3):243-271, 1973. Google Scholar
  5. Luc Dartois and Charles Paperman. Two-variable first order logic with modular predicates over words. In Proceedings of the 30th International Symposium on Theoretical Aspects of Computer Science, STACS'13, Leibniz International Proceedings in Informatics (LIPIcs), pages 329-340. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. Google Scholar
  6. Volker Diekert, Paul Gastin, and Manfred Kufleitner. A survey on small fragments of first-order logic over finite words. International Journal of Foundations of Computer Science, 19(3):513-548, 2008. Google Scholar
  7. Volker Diekert, Martin Horsch, and Manfred Kufleitner. On first-order fragments for Mazurkiewicz traces. Fundamenta Informaticae, 80(1-3):1-29, 2007. Google Scholar
  8. Volker Diekert and Manfred Kufleitner. Fragments of first-order logic over infinite words. Theory of Computing Systems (ToCS), 48(3):486-516, 2011. Google Scholar
  9. Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-order logic with two variables and unary temporal logic. Information and Computation, 179(2):279-295, 2002. Google Scholar
  10. James Alexander Green. On the structure of semigroups. Annals of Mathematics, 54(1):163-172, 1951. Google Scholar
  11. Hans W. Kamp. Tense Logic and the Theory of Linear Order. Phd thesis, Computer Science Department, University of California at Los Angeles, USA, 1968. Google Scholar
  12. Robert Knast. A semigroup characterization of dot-depth one languages. RAIRO - Theoretical Informatics and Applications, 17(4):321-330, 1983. Google Scholar
  13. Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing. Two-variable logic with a between relation. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'16, pages 106-115, 2016. Google Scholar
  14. Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing. An algebraic decision procedure for two-variable logic with a between relation. In 27th EACSL Annual Conference on Computer Science Logic, CSL'18, Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  15. Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing. Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership. Logical Methods in Computer Science, Volume 16, Issue 3, 2020. Google Scholar
  16. Robert McNaughton and Seymour A. Papert. Counter-Free Automata. MIT Press, 1971. Google Scholar
  17. Jean-Éric Pin. Varieties of Formal Languages. North Oxford Academic, 1986. Google Scholar
  18. Jean-Éric Pin and Pascal Weil. Polynomial closure and unambiguous product. Theory of Computing Systems, 30(4):383-422, 1997. Google Scholar
  19. Jean-Éric Pin. An explicit formula for the intersection of two polynomials of regular languages. In Proceedings of the 17th International Conference on Developments in Language Theory, DLT'13, volume 7907 of Lecture Notes in Computer Science, pages 31-45. Springer, 2013. Google Scholar
  20. Jean-Éric Pin. Mathematical foundations of automata theory. Lecture notes, in preparation, 2022. URL: https://www.irif.fr/~jep/PDF/MPRI/MPRI.pdf.
  21. Thomas Place. The amazing mixed polynomial closure and its applications to two-variable first-order logic. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'22, 2022. Google Scholar
  22. Thomas Place and Marc Zeitoun. Separating without any ambiguity. In 45th International Colloquium on Automata, Languages, and Programming, ICALP'18, Leibniz International Proceedings in Informatics (LIPIcs), pages 137:1-137:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  23. Thomas Place and Marc Zeitoun. Generic results for concatenation hierarchies. Theory of Computing Systems (ToCS), 63(4):849-901, 2019. Selected papers from CSR'17. Google Scholar
  24. Thomas Place and Marc Zeitoun. Going higher in first-order quantifier alternation hierarchies on words. Journal of the ACM, 66(2):12:1-12:65, 2019. Google Scholar
  25. Thomas Place and Marc Zeitoun. On all things star-free. In Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, ICALP'19, Leibniz International Proceedings in Informatics (LIPIcs), pages 126:1-126:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  26. Thomas Place and Marc Zeitoun. How many times do you need to go back to the future in unary temporal logic? In Proceedings of the 15th Latin American Symposium on Theoretical Informatics, LATIN'22, Lecture Notes in Computer Science. Springer, 2022. Google Scholar
  27. Thomas Place and Marc Zeitoun. All about unambiguous polynomial closure. TheoretiCS, 2(11):1-74, 2023. URL: https://doi.org/10.46298/theoretics.23.11.
  28. Thomas Place and Marc Zeitoun. Closing star-free closure, 2023. URL: https://arxiv.org/abs/2307.09376.
  29. Thomas Place and Marc Zeitoun. A generic characterization of generalized unary temporal logic and two-variable first-order logic, 2023. URL: https://arxiv.org/abs/2307.09349.
  30. Marcel Paul Schützenberger. On finite monoids having only trivial subgroups. Information and Control, 8(2):190-194, 1965. Google Scholar
  31. Marcel Paul Schützenberger. Sur certaines opérations de fermeture dans les langages rationnels. Symposia Mathematica, XV:245-253, 1975. Google Scholar
  32. Marcel Paul Schützenberger. Sur le produit de concaténation non ambigu. Semigroup Forum, 13:47-75, 1976. Google Scholar
  33. Imre Simon. Piecewise testable events. In Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, pages 214-222. Springer, 1975. Google Scholar
  34. Howard Straubing. Aperiodic homomorphisms and the concatenation product of recognizable sets. Journal of Pure and Applied Algebra, 15(3):319-327, 1979. Google Scholar
  35. Pascal Tesson and Denis Thérien. Diamonds are forever: The variety DA. In Semigroups, Algorithms, Automata and Languages, pages 475-500. World Scientific, 2002. Google Scholar
  36. Denis Thérien and Thomas Wilke. Over words, two variables are as powerful as one quantifier alternation. In Proceedings of the 30th Annual ACM Symposium on Theory of Computing, STOC'98, pages 234-240. ACM, 1998. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact