Document Open Access Logo

Expressiveness Results for an Inductive Logic of Separated Relations

Authors Radu Iosif , Florian Zuleger

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.20.pdf
  • Filesize: 0.89 MB
  • 20 pages

Document Identifiers

Author Details

Radu Iosif
  • Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, 38000, France
Florian Zuleger
  • Institute of Logic and Computation, Technische Universität Wien, Austria

Funding

  • Iosif, Radu: The first author wishes to acknowledge the support of the French National Research Agency project Non-Aggregative Resource COmpositions (NARCO) under grant number ANR-21-CE48-0011.

Cite As Get BibTex

Radu Iosif and Florian Zuleger. Expressiveness Results for an Inductive Logic of Separated Relations. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CONCUR.2023.20

Abstract

In this paper we study a Separation Logic of Relations (SLR) and compare its expressiveness to (Monadic) Second Order Logic [(M)SO]. SLR is based on the well-known Symbolic Heap fragment of Separation Logic, whose formulæare composed of points-to assertions, inductively defined predicates, with the separating conjunction as the only logical connective. SLR generalizes the Symbolic Heap fragment by supporting general relational atoms, instead of only points-to assertions. In this paper, we restrict ourselves to finite relational structures, and hence only consider Weak (M)SO, where quantification ranges over finite sets. Our main results are that SLR and MSO are incomparable on structures of unbounded treewidth, while SLR can be embedded in SO in general. Furthermore, MSO becomes a strict subset of SLR, when the treewidth of the models is bounded by a parameter and all vertices attached to some hyperedge belong to the interpretation of a fixed unary relation symbol. We also discuss the problem of identifying a fragment of SLR that is equivalent to MSO over models of bounded treewidth.

Subject Classification

ACM Subject Classification
  • Theory of computation → Separation logic
Keywords
  • Separation Logic
  • Model Theory
  • Monadic Second Order Logic
  • Treewidth

Metrics

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

Related Versions

References

  1. Serge Abiteboul, Peter Buneman, and Dan Suciu. Data on the Web: From Relations to Semistructured Data and XML. Morgan Kaufmann, 2000. Google Scholar
  2. Peter Aczel. An introduction to inductive definitions. In Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 739-782. Elsevier, 1977. URL: https://doi.org/10.1016/S0049-237X(08)71120-0.
  3. Isolde Adler, Martin Grohe, and Stephan Kreutzer. Computing excluded minors. In Proceedings of the Nineteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA '08, pages 641-650, USA, 2008. Society for Industrial and Applied Mathematics. Google Scholar
  4. Emma Ahrens, Marius Bozga, Radu Iosif, and Joost-Pieter Katoen. Reasoning about distributed reconfigurable systems. Proc. ACM Program. Lang., 6(OOPSLA2):145-174, 2022. URL: https://doi.org/10.1145/3563293.
  5. Timos Antonopoulos and Anuj Dawar. Separating graph logic from mso. In Luca de Alfaro, editor, Foundations of Software Science and Computational Structures, pages 63-77, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  6. Mikołaj Bojańczyk and Michał Pilipczuk. Definability equals recognizability for graphs of bounded treewidth. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 407-416, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2933575.2934508.
  7. Marius Bozga, Lucas Bueri, and Radu Iosif. Decision problems in a logic for reasoning about reconfigurable distributed systems. In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pages 691-711. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-10769-6_40.
  8. Marius Bozga, Lucas Bueri, and Radu Iosif. Decision problems in a logic for reasoning about reconfigurable distributed systems. CoRR, abs/2202.09637, 2022. URL: https://arxiv.org/abs/2202.09637.
  9. Marius Bozga, Lucas Bueri, and Radu Iosif. On an invariance problem for parameterized concurrent systems. In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors, 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland, volume 243 of LIPIcs, pages 24:1-24:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.24.
  10. Marius Bozga, Radu Iosif, and Joseph Sifakis. Verification of component-based systems with recursive architectures. Theor. Comput. Sci., 940(Part):146-175, 2023. URL: https://doi.org/10.1016/j.tcs.2022.10.022.
  11. Rémi Brochenin, Stéphane Demri, and Étienne Lozes. On the almighty wand. Inf. Comput., 211:106-137, 2012. Google Scholar
  12. James Brotherston, Carsten Fuhs, Juan Antonio Navarro Pérez, and Nikos Gorogiannis. A decision procedure for satisfiability in separation logic with inductive predicates. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14-18, 2014, pages 25:1-25:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603091.
  13. James Brotherston, Nikos Gorogiannis, Max I. Kanovich, and Reuben Rowe. Model checking for symbolic-heap separation logic with inductive predicates. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20-22, 2016, pages 84-96. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837621.
  14. Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. J. ACM, 58(6), December 2011. URL: https://doi.org/10.1145/2049697.2049700.
  15. Cristiano Calcagno, Philippa Gardner, and Matthew Hague. From separation logic to first-order logic. In Foundations of Software Science and Computational Structures, pages 395-409, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  16. Cristiano Calcagno, Peter W. O'Hearn, and Hongseok Yang. Local action and abstract separation logic. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings, pages 366-378. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/LICS.2007.30.
  17. Cristiano Calcagno, Hongseok Yang, and Peter W. O'Hearn. Computability and complexity results for a spatial assertion language for data structures. In Ramesh Hariharan, Madhavan Mukund, and V. Vinay, editors, FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 21st Conference, Bangalore, India, December 13-15, 2001, Proceedings, volume 2245 of Lecture Notes in Computer Science, pages 108-119. Springer, 2001. Google Scholar
  18. Luca Cardelli, Philippa Gardner, and Giorgio Ghelli. A Spatial Logic for Querying Graphs. In Peter Widmayer, Francisco Triguero Ruiz, Rafael Morales Bueno, Matthew Hennessy, Stephan Eidenbenz, and Ricardo Conejo, editors, Proceedings of the 29superscriptth International Colloquium on Automata, Languages and Programming (ICALP'02), volume 2380 of Lecture Notes in Computer Science, pages 597-610. Springer, July 2002. URL: https://doi.org/10.1007/3-540-45465-9_51.
  19. Luca Cardelli and Andrew D. Gordon. Anytime, anywhere: Modal logics for mobile ambients. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '00, pages 365-377, New York, NY, USA, 2000. Association for Computing Machinery. URL: https://doi.org/10.1145/325694.325742.
  20. Matthew Collinson, Kevin McDonald, and David J. Pym. A substructural logic for layered graphs. J. Log. Comput., 24(4):953-988, 2014. URL: https://doi.org/10.1093/logcom/exu002.
  21. Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, and James Worrell. Tractable reasoning in a fragment of separation logic. In Joost-Pieter Katoen and Barbara König, editors, CONCUR 2011 - Concurrency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings, volume 6901 of Lecture Notes in Computer Science, pages 235-249. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23217-6_16.
  22. Bruno Courcelle. The monadic second-order logic of graphs. i. recognizable sets of finite graphs. Information and Computation, 85(1):12-75, 1990. URL: https://doi.org/10.1016/0890-5401(90)90043-H.
  23. Bruno Courcelle. The monadic second-order logic of graphs VII: graphs as relational structures. Theor. Comput. Sci., 101(1):3-33, 1992. URL: https://doi.org/10.1016/0304-3975(92)90148-9.
  24. Bruno Courcelle. Monadic second-order definable graph transductions: A survey. Theor. Comput. Sci., 126(1):53-75, 1994. URL: https://doi.org/10.1016/0304-3975(94)90268-2.
  25. Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2012. URL: https://doi.org/10.1017/CBO9780511977619.
  26. Anuj Dawar, Philippa Gardner, and Giorgio Ghelli. Expressiveness and Complexity of Graph Logic. Information and Computation, 205(3):263-310, February 2007. URL: https://doi.org/10.1016/j.ic.2006.10.006.
  27. Pierpaolo Degano, Rocco De Nicola, and José Meseguer, editors. Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday, volume 5065 of Lecture Notes in Computer Science. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-68679-8.
  28. Stéphane Demri and Morgan Deters. Expressive completeness of separation logic with two variables and no separating conjunction. ACM Trans. Comput. Log., 17(2):12, 2016. Google Scholar
  29. Stéphane Demri, Étienne Lozes, and Alessio Mansutti. The effects of adding reachability predicates in quantifier-free separation logic. ACM Trans. Comput. Log., 22(2):14:1-14:56, 2021. URL: https://doi.org/10.1145/3448269.
  30. Reinhard Diestel. Graph Theory, 4th Edition, volume 173 of Graduate texts in mathematics. Springer, 2012. Google Scholar
  31. Cezara Drăgoi, Constantin Enea, and Mihaela Sighireanu. Local shape analysis for overlaid data structures. In Francesco Logozzo and Manuel Fähndrich, editors, Static Analysis, pages 150-171, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  32. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Perspectives in Mathematical Logic. Springer, 1995. Google Scholar
  33. Mnacho Echenim, Radu Iosif, and Nicolas Peltier. The bernays-schönfinkel-ramsey class of separation logic with uninterpreted predicates. ACM Trans. Comput. Log., 21(3):19:1-19:46, 2020. Google Scholar
  34. Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment. In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1-20:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.20.
  35. Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Unifying decidable entailments in separation logic with inductive definitions. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 183-199. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_11.
  36. Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules. Inf. Process. Lett., 173:106169, 2022. URL: https://doi.org/10.1016/j.ipl.2021.106169.
  37. Diego Figueira and Leonid Libkin. Path logics for querying graphs: Combining expressiveness and efficiency. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 329-340. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.39.
  38. Jörg Flum and Martin Grohe. Parameterized Complexity Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2006. URL: https://doi.org/10.1007/3-540-29953-X.
  39. S. Greibach. A note on undecidable properties of formal languages. Math. Systems Theory, 2:1-6, 1968. URL: https://doi.org/10.1007/BF01691341.
  40. Neil Immerman. Second-Order Logic and Fagin’s Theorem, pages 113-124. Springer New York, New York, NY, 1999. URL: https://doi.org/10.1007/978-1-4612-0539-5_8.
  41. Radu Iosif, Adam Rogalewicz, and Jirí Simácek. The tree width of separation logic with recursive definitions. In Maria Paola Bonacina, editor, Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, volume 7898 of Lecture Notes in Computer Science, pages 21-38. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38574-2_2.
  42. Radu Iosif and Florian Zuleger. Expressiveness results for an inductive logic of separated relations, 2023. URL: https://arxiv.org/abs/2307.02381.
  43. Samin S. Ishtiaq and Peter W. O'Hearn. BI as an assertion language for mutable data structures. In Chris Hankin and Dave Schmidt, editors, Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001, pages 14-26. ACM, 2001. URL: https://doi.org/10.1145/360204.375719.
  44. Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, and Florian Zuleger. Unified reasoning about robustness properties of symbolic-heap separation logic. In European Symposium on Programming (ESOP), volume 10201 of Lecture Notes in Computer Science, pages 611-638. Springer, 2017. Google Scholar
  45. Neil D. Jones and Steven S. Muchnick. A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '82, pages 66-74, New York, NY, USA, 1982. Association for Computing Machinery. URL: https://doi.org/10.1145/582153.582161.
  46. Jens Katelaan, Dejan Jovanovic, and Georg Weissenbacher. A separation logic with data: Small models and automation. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, volume 10900 of Lecture Notes in Computer Science, pages 455-471. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94205-6_30.
  47. Jens Katelaan and Florian Zuleger. Beyond symbolic heaps: Deciding separation logic with inductive definitions. In Elvira Albert and Laura Kovács, editors, LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing, pages 390-408. EasyChair, 2020. URL: https://doi.org/10.29007/vkmj.
  48. Viktor Kuncak and Martin Rinard. Generalized records and spatial conjunction in role logic. In Static Analysis, pages 361-376, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  49. Viktor Kuncak and Martin C. Rinard. On spatial conjunction as second-order logic. CoRR, cs.LO/0410073, 2004. URL: http://arxiv.org/abs/cs.LO/0410073.
  50. Étienne Lozes. Expressivité des logiques spatiales. Thèse de doctorat, Laboratoire de l'Informatique du Parallélisme, ENS Lyon, France, November 2004. URL: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PhD-lozes.ps.
  51. Johann A. Makowsky. Algorithmic uses of the feferman-vaught theorem. Ann. Pure Appl. Log., 126(1-3):159-213, 2004. Google Scholar
  52. Alessio Mansutti. Logiques de séparation : complexité, expressivité, calculs. (Reasoning with separation logics : complexity, expressive power, proof systems). PhD thesis, University of Paris-Saclay, France, 2020. URL: https://tel.archives-ouvertes.fr/tel-03094373.
  53. Christoph Matheja, Jens Pagel, and Florian Zuleger. A decision procedure for guarded separation logic complete entailment checking for separation logic with inductive definitions. ACM Trans. Comput. Log., 24(1):1:1-1:76, 2023. URL: https://doi.org/10.1145/3534927.
  54. Peter W. O'Hearn and David J. Pym. The logic of bunched implications. Bull. Symb. Log., 5(2):215-244, 1999. Google Scholar
  55. M. R. Fellows R. G. Downey. Parameterized Complexity. Springer New York, NY, 1999. URL: https://doi.org/10.1007/978-1-4612-0515-9.
  56. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages 55-74. IEEE Computer Society, 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  57. D. Seese. The structure of the models of decidable monadic theories of graphs. Annals of Pure and Applied Logic, 53(2):169-195, 1991. URL: https://doi.org/10.1016/0168-0072(91)90054-P.
  58. Dirk van Dalen. Logic and structure (3. ed.). Universitext. Springer, 1994. Google Scholar
  59. Moshe Y. Vardi. The complexity of relational query languages (extended abstract). In Proceedings of the 14th Annual ACM Symposium on Theory of Computing, May 5-7, 1982, San Francisco, California, USA, pages 137-146. ACM, 1982. 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