Document Open Access Logo

Local First-Order Logic with Two Data Values

Authors Benedikt Bollig, Arnaud Sangnier, Olivier Stietel

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2021.39.pdf
  • Filesize: 0.78 MB
  • 15 pages

Document Identifiers

Author Details

Benedikt Bollig
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, France
Arnaud Sangnier
  • IRIF, Université de Paris, CNRS, France
Olivier Stietel
  • IRIF, Université de Paris, CNRS, France
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, France

Funding

Partly supported by ANR FREDDA (ANR-17-CE40-0013).

Acknowledgements

The authors would like to thank the reviewers for their careful reading of the paper and their helpful comments.

Cite AsGet BibTex

Benedikt Bollig, Arnaud Sangnier, and Olivier Stietel. Local First-Order Logic with Two Data Values. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 39:1-39:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSTTCS.2021.39

Abstract

We study first-order logic over unordered structures whose elements carry two data values from an infinite domain. Data values can be compared wrt. equality so that the formalism is suitable to specify the input-output behavior of various distributed algorithms. As the logic is undecidable in general, we introduce a family of local fragments that restrict quantification to neighborhoods of a given reference point. Our main result establishes decidability of the satisfiability problem for one of these non-trivial local fragments. On the other hand, already slightly more general local logics turn out to be undecidable. Altogether, we draw a landscape of formalisms that are suitable for the specification of systems with data and open up new avenues for future research.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • first-order logic
  • data values
  • specification of distributed algorithms

Metrics

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

Related Versions

References

  1. C. Aiswarya, B. Bollig, and P. Gastin. An automata-theoretic approach to the verification of distributed algorithms. Inf. Comput., 259(Part 3):305-327, 2018. Google Scholar
  2. B. Bednarczyk and P. Witkowski. A Note on C² Interpreted over Finite Data-Words. In 27th International Symposium on Temporal Representation and Reasoning, TIME 2020, September 23-25, 2020, Bozen-Bolzano, Italy, volume 178 of LIPIcs, pages 17:1-17:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.TIME.2020.17.
  3. H. Björklund and M. Bojanczyk. Shuffle expressions and words with nested data. In Ludek Kucera and Antonín Kucera, editors, Mathematical Foundations of Computer Science 2007, 32nd International Symposium, MFCS 2007, Ceský Krumlov, Czech Republic, August 26-31, 2007, Proceedings, volume 4708 of Lecture Notes in Computer Science, pages 750-761. Springer, 2007. Google Scholar
  4. R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, and J. Widder. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015. Google Scholar
  5. M. Bojanczyk, C. David, A. Muscholl, T. Schwentick, and L. Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log., 12(4):27:1-27:26, 2011. Google Scholar
  6. M. Bojanczyk, A. Muscholl, T. Schwentick, and L. Segoufin. Two-variable logic on data trees and XML reasoning. J. ACM, 56(3), 2009. Google Scholar
  7. B. Bollig, P. Bouyer, and F. Reiter. Identifiers in registers - describing network algorithms with logic. In FOSSACS'19, volume 11425 of LNCS, pages 115-132. Springer, 2019. Google Scholar
  8. B. Bollig and D. Kuske. An optimal construction of hanf sentences. J. Appl. Log., 10(2):179-186, 2012. URL: https://doi.org/10.1016/j.jal.2012.01.002.
  9. E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997. Google Scholar
  10. N. Decker, P. Habermehl, M. Leucker, and D. Thoma. Ordered navigation on multi-attributed data words. In Paolo Baldan and Daniele Gorla, editors, CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings, volume 8704 of Lecture Notes in Computer Science, pages 497-511. Springer, 2014. Google Scholar
  11. E. A. Emerson and K. S. Namjoshi. On reasoning about rings. Int. J. Found. Comput. Sci., 14(4):527-550, 2003. Google Scholar
  12. J. Esparza. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In STACS'14), volume 25 of LIPIcs, pages 1-10. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. Google Scholar
  13. W. Fokkink. Distributed Algorithms: An Intuitive Approach. MIT Press, 2013. Google Scholar
  14. S. Grumbach and Z. Wu. Logical locality entails frugal distributed computation over graphs (extended abstract). In WG'09, volume 5911 of LNCS, pages 154-165. Springer, 2009. Google Scholar
  15. W. Hanf. Model-theoretic methods in the study of elementary logic. In J.W. Addison, L. Henkin, and A. Tarski, editors, The Theory of Models, pages 132-145. North Holland, 1965. Google Scholar
  16. A. Janiczak. Undecidability of some simple formalized theories. Fundamenta Mathematicae, 40:131-139, 1953. Google Scholar
  17. A. Kara, T. Schwentick, and T. Zeume. Temporal logics on words with multiple data values. In Kamal Lodaya and Meena Mahajan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India, volume 8 of LIPIcs, pages 481-492. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. Google Scholar
  18. E. Kieronski. Results on the guarded fragment with equivalence or transitive relations. In C.-H. Luke Ong, editor, CSL'05, volume 3634 of LNCS, pages 309-324. Springer, 2005. Google Scholar
  19. E. Kieronski, J. Michaliszyn, I. Pratt-Hartmann, and L. Tendera. Two-variable first-order logic with equivalence closure. In LICS'12, pages 431-440. IEEE, 2012. Google Scholar
  20. E. Kieronski and L. Tendera. On finite satisfiability of two-variable first-order logic with equivalence relations. In LICS'09, pages 123-132. IEEE, 2009. Google Scholar
  21. I. V. Konnov, H. Veith, and J. Widder. What you always wanted to know about model checking of fault-tolerant distributed algorithms. In PSI'15 in Memory of Helmut Veith, volume 9609 of LNCS, pages 6-21. Springer, 2015. Google Scholar
  22. L. Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. Google Scholar
  23. N. A. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers Inc., 1996. Google Scholar
  24. A. Manuel and T. Zeume. Two-variable logic on 2-dimensional structures. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 484-499. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. Google Scholar
  25. M. Otto. Two-variable first-order logic over ordered domains. Journal of Symbolic Logic, 66:685-702, 2001. Google Scholar
  26. L. Segoufin. Automata and logics for words and trees over an infinite alphabet. In CSL'06, volume 4207 of LNCS, pages 41-57. Springer, 2006. Google Scholar
  27. T. Tan. Extending two-variable logic on data trees with order on data values and its automata. ACM Trans. Comput. Log., 15(1):8:1-8:39, 2014. 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 Imprint Privacy Contact