Document Open Access Logo

Two-Variable Logic over Countable Linear Orderings

Authors Amaldev Manuel, A. V. Sreejith

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2016.66.pdf
  • Filesize: 446 kB
  • 13 pages

Document Identifiers

Subject Classification

Keywords
  • circ-monoids
  • countable linear orderings
  • FO^2

Metrics

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

Abstract

We study the class of languages of finitely-labelled countable linear orderings definable in  two-variable first-order logic. We give a number of characterisations, in particular an algebraic one in terms of circle monoids, using equations. This generalises the corresponding characterisation, namely variety DA, over finite words to the countable case. A corollary is that the membership in this class is decidable: for instance given an MSO formula  it is possible to check if there is an equivalent two-variable logic formula over countable linear orderings. In addition, we  prove that the satisfiability problems for two-variable logic over arbitrary, countable, and scattered linear orderings are NEXPTIME-complete.

Cite As Get BibTex

Amaldev Manuel and A. V. Sreejith. Two-Variable Logic over Countable Linear Orderings. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 66:1-66:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.MFCS.2016.66

Author Details

Amaldev Manuel
A. V. Sreejith

References

  1. Nicolas Bedon, Alexis Bès, Olivier Carton, and Chloe Rispal. Logic and rational languages of words indexed by linear orderings. Theory Comput. Syst., 46(4):737-760, 2010. Google Scholar
  2. Alexis Bès and Olivier Carton. Algebraic characterization of FO for scattered linear orderings. In Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, pages 67-81, 2011. Google Scholar
  3. Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log., 12(4):27, 2011. Google Scholar
  4. Olivier Carton, Thomas Colcombet, and Gabriele Puppis. Regular languages of words over countable linear orderings. In Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Proceedings, Part II, pages 125-136, 2011. Google Scholar
  5. Thomas Colcombet. Factorization forests for infinite words and applications to countable scattered linear orderings. Theor. Comput. Sci., 411(4-5):751-764, 2010. Google Scholar
  6. Thomas Colcombet and A. V. Sreejith. Limited set quantifiers over countable linear orderings. In Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Proceedings, Part II, pages 146-158, 2015. Google Scholar
  7. Julien Cristau. Automata and temporal logic over arbitrary linear time. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2009, pages 133-144, 2009. Google Scholar
  8. Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-order logic with two variables and unary temporal logic. Inf. Comput., 179(2):279-295, 2002. Google Scholar
  9. Martin Fürer. The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems). In Logic and Machines: Decision Problems and Complexity, Proceedings of Symposium Rekursive Kombinatorik, pages 312-319, 1983. Google Scholar
  10. Erich Grädel, Phokion G. Kolaitis, and Moshe Y. Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 3(1):53-69, 1997. Google Scholar
  11. Manfred Kufleitner and Pascal Weil. On FO2 quantifier alternation over words. In Mathematical Foundations of Computer Science 2009, 34th International Symposium, MFCS 2009, pages 513-524, 2009. Google Scholar
  12. Manfred Kufleitner and Pascal Weil. The FO2 alternation hierarchy is decidable. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, pages 426-439, 2012. Google Scholar
  13. Amaldev Manuel. Two variables and two successors. In Mathematical Foundations of Computer Science 2010, 35th International Symposium, MFCS, pages 513-524, 2010. Google Scholar
  14. Amaldev Manuel and Thomas Zeume. Two-variable logic on 2-dimensional structures. In Computer Science Logic 2013 (CSL 2013), CSL, pages 484-499, 2013. Google Scholar
  15. Martin Otto. Two variable first-order logic over ordered domains. J. Symb. Log., 66(2):685-702, 2001. Google Scholar
  16. Jean-Éric Pin. Mathematical foundations of automata theory. Google Scholar
  17. Jean-Eric Pin and Pascal Weil. Polynomial closure and unambiguous product. In Automata, Languages and Programming, 22nd International Colloquium, ICALP95, Proceedings, pages 348-359, 1995. Google Scholar
  18. Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1-35, 1969. Google Scholar
  19. Alexander Rabinovich. Temporal logics over linear time domains are in PSPACE. Inf. Comput., 210:40-67, 2012. Google Scholar
  20. Joseph G. Rosenstein. Linear orderings. Academic Press New York, 1981. Google Scholar
  21. Marcel Paul Schützenberger. On finite monoids having only trivial subgroups. Information and Control, 8:190-194, 1965. Google Scholar
  22. Thomas Schwentick, Denis Thérien, and Heribert Vollmer. Partially-ordered two-way automata: A new characterization of DA. In Developments in Language Theory, 5th International Conference, DLT 2001, pages 239-250, 2001. Google Scholar
  23. Thomas Schwentick and Thomas Zeume. Two-variable logic with two order relations. Logical Methods in Computer Science, 8(1), 2012. Google Scholar
  24. S.Shelah. The monadic theory of order. Ann. of Math., 102:379-419, 1975. Google Scholar
  25. Pascal Tesson and Denis Therien. Diamonds are forever: The variety DA. In Semigroups, Algorithms, Automata and Languages, pages 475-500. World Scientific, 2002. Google Scholar
  26. Denis Thérien and Thomas Wilke. Over words, two variables are as powerful as one quantifier alternation. In Proceedings of the Thirtieth Annual ACM Symposium on Theory of Computing, STOC'98, pages 234-240. ACM, 1998. Google Scholar
  27. Philipp Weis and Neil Immerman. Structure theorem and strict alternation hierarchy for FO^2 on words. Logical Methods in Computer Science, 5(3), 2009. 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