Document Open Access Logo

An Algebraic Decision Procedure for Two-Variable Logic with a Between Relation

Authors Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, Howard Straubing

PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.28.pdf
  • Filesize: 0.59 MB
  • 17 pages

Document Identifiers

Author Details

Andreas Krebs
  • Universität Tübingen, Germany
Kamal Lodaya
  • The Institute of Mathematical Sciences, Chennai, India
Paritosh K. Pandya
  • Tata Institute of Fundamental Research, Mumbai, India
Howard Straubing
  • Boston College, USA

Cite As Get BibTex

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 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CSL.2018.28

Abstract

In earlier work (LICS 2016), the authors introduced two-variable first-order logic supplemented by a binary relation that allows one to say that a letter appears between two positions. We found an effective algebraic criterion that is a necessary condition for definability in this logic, and conjectured that the criterion is also sufficient, although we proved this only in the case of two-letter alphabets. Here we prove the general conjecture. The proof is quite different from the arguments in the earlier work, and required the development of novel techniques concerning factorizations of words. We extend the results to binary relations specifying that a factor appears between two positions.

Subject Classification

ACM Subject Classification
  • Theory of computation → Algebraic language theory
  • Theory of computation → Finite Model Theory
Keywords
  • two-variable logic
  • finite model theory
  • algebraic automata theory

Metrics

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

References

  1. Jorge Almeida. A syntactical proof of the locality of DA. Int. J. Alg. Comput., 6:165-177, 1996. Google Scholar
  2. Janusz Brzozowski. A generalization of finiteness. Semigr. Forum, 13:239-251, 1977. Google Scholar
  3. Rina Cohen and Janusz Brzozowski. Dot-depth of star-free events. J. Comput. Syst. Sci., 5(1):1-16, 1971. Google Scholar
  4. Volker Diekert, Paul Gastin, and Manfred Kufleitner. First-order logic over finite words. Int. J. Found. Comp. Sci., 19:513-548, 2008. Google Scholar
  5. Kousha Etessami, Moshe Vardi, and Thomas Wilke. First-order logic with two variables and unary temporal logic. Inf. Comput., 179(2):279-295, 2002. Google Scholar
  6. Johan Anthony Willem Kamp. Tense logic and the theory of linear order. UCLA, 1968. PhD thesis. Google Scholar
  7. Robert Knast. A semigroup characterization of dot-depth one languages. Inf. Theor. Appl., 17(4):321-330, 1983. Google Scholar
  8. Andreas Krebs, Kamal Lodaya, Paritosh Pandya, and Howard Straubing. Two-variable logic with a between relation. In Martin Grohe, Erik Koskinen, and Natarajan Shankar, editors, Proc. 31st LICS, New York, pages 106-115. ACM/IEEE, 2016. Google Scholar
  9. Robert McNaughton and Seymour Papert. Counter-free automata. MIT Press, 1971. Google Scholar
  10. Jean-Éric Pin. Varieties of formal languages. Plenum, 1986. Google Scholar
  11. Thomas Place and Luc Segoufin. Decidable characterization of fo²(< ,+1) and locality of DA. Preprint, ENS Cachan, 2014. Google Scholar
  12. Thomas Place and Marc Zeitoun. Going higher in the first-order quantifier alternation hierarchy on words. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Proc. 41st Icalp, Part 2, Copenhagen, volume 8573 of LNCS, pages 342-353, 2014. Google Scholar
  13. Thomas Place and Marc Zeitoun. Separation and the successor relation. In Ernst W. Mayr and Nicolas Ollinger, editors, Proc. 32nd Stacs, Garching, volume 30 of Lipics, pages 662-675, 2015. Google Scholar
  14. Marcel-Paul Schützenberger. On finite monoids having only trivial subgroups. Inf. Contr., 8:190-194, 1965. Google Scholar
  15. Marcel-Paul Schützenberger. Sur le produit de concaténation non ambigu. Semigr. Forum, 13:47-75, 1976. Google Scholar
  16. A. Prasad Sistla and Edmund Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, 1985. Google Scholar
  17. Howard Straubing. Finite semigroup varieties of the form V*D. J. Pure Appl. Alg., 36:53-94, 1985. Google Scholar
  18. Howard Straubing. Finite automata, formal languages, and circuit complexity. Birkhäuser, 1994. Google Scholar
  19. Pascal Tesson and Denis Thérien. Logic meets algebra: the case of regular languages. Log. Meth. Comp. Sci., 3(1:4):1-37, 2007. Google Scholar
  20. Denis Thérien and Thomas Wilke. Over words, two variables are as powerful as one quantifier alternation. In Jeffrey Vitter, editor, Proc. 30th STOC, Dallas, pages 234-240. ACM, 1998. Google Scholar
  21. Bret Tilson. Categories as algebra. J. Pure Appl. Alg., 48:83-198, 1987. Google Scholar
  22. Pascal Weil. Some results on the dot-depth hierarchy. Semigr. Forum, 46:352-370, 1993. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact