Document Open Access Logo

Iterating Non-Aggregative Structure Compositions

Authors Marius Bozga , Radu Iosif , Florian Zuleger

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2025.18.pdf
  • Filesize: 0.95 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Grammars and context-free languages
Keywords
  • Hyperedge replacement
  • Tree-width

Metrics

Abstract

An aggregative composition is a binary operation obeying the principle that the whole is determined by the sum of its parts. The development of graph algebras, on which the theory of formal graph languages is built, relies on aggregative compositions that behave like disjoint union, except for a set of well-marked interface vertices from both sides, that are joined. The same style of composition has been considered in the context of relational structures, that generalize graphs and use constant symbols to label the interface.
In this paper, we study a non-aggregative composition operation, called fusion, that joins non-deterministically chosen elements from disjoint structures. The sets of structures obtained by iteratively applying fusion do not always have bounded tree-width, even when starting from a tree-width bounded set. First, we prove that the problem of the existence of a bound on the tree-width of the closure of a given set under fusion is decidable, when the input set is described inductively by a finite hyperedge-replacement (HR) grammar, written using the operations of aggregative composition, forgetting and renaming of constants. Such sets are usually called context-free. Second, assuming that the closure under fusion of a context-free set has bounded tree-width, we show that it is the language of an effectively constructible HR grammar. A possible application of the latter result is the possiblity of checking whether all structures from a non-aggregatively closed set having bounded tree-width satisfy a given monadic second order logic formula.

Cite As Get BibTex

Marius Bozga, Radu Iosif, and Florian Zuleger. Iterating Non-Aggregative Structure Compositions. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSTTCS.2025.18

Author Details

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

Funding

Marius Bozga and Radu Iosif wish to acknowledge the support of the French National Research Agency project Non-Aggregative Resource COmpositions (NARCO) under grant number ANR-21-CE48-0011. Florian Zuleger wishes to acknowledge the support of the FWF project AUTOSARD: "Automated Sublinear Amortised Resource Analysis of Data Structures" No. P36623 and the project VASSAL: "Verification and Analysis for Safety and Security of Applications in Life" funded by the European Union under Horizon Europe WIDERA Coordination and Support Action/Grant Agreement No. 101160022.

References

  1. 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.
  2. Cristiano Calcagno, Philippa Gardner, and Uri Zarfaty. Context logic and tree update. In Jens Palsberg and Martín Abadi, editors, Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, pages 271-282. ACM, 2005. URL: https://doi.org/10.1145/1040305.1040328.
  3. Cristiano Calcagno, Philippa Gardner, and Uri Zarfaty. Context logic as modal logic: completeness and parametric inexpressivity. In Martin Hofmann and Matthias Felleisen, editors, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pages 123-134. ACM, 2007. URL: https://doi.org/10.1145/1190216.1190236.
  4. 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 29th 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.
  5. Hubert Comon, Max Dauchet, Rémi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Löding, Sophie Tison, and Marc Tommasi. Tree Automata Techniques and Applications. HAL, 2008. URL: https://inria.hal.science/hal-03367725.
  6. 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.
  7. 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.
  8. 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.
  9. Simon Docherty and David J. Pym. Intuitionistic layered graph logic: Semantics and proof theory. Log. Methods Comput. Sci., 14(4), 2018. URL: https://doi.org/10.23638/LMCS-14(4:11)2018.
  10. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Perspectives in Mathematical Logic. Springer, 1995. Google Scholar
  11. 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.
  12. Radu Iosif and Florian Zuleger. Expressiveness results for an inductive logic of separated relations. In Guillermo A. Pérez and Jean-François Raskin, editors, 34th International Conference on Concurrency Theory (CONCUR 2023), volume 279 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1-20:20, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2023.20.
  13. 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.
  14. 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. URL: https://doi.org/10.1007/978-3-540-27864-1_26.
  15. Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In Proceedings of the 15th International Workshop on Computer Science Logic, CSL '01, pages 1-19, 2001. URL: https://doi.org/10.1007/3-540-44802-0_1.
  16. David J. Pym, Peter W. O'Hearn, and Hongseok Yang. Possible worlds and resources: the semantics of bi. Theoretical Computer Science, 315(1):257-305, 2004. Mathematical Foundations of Programming Semantics. URL: https://doi.org/10.1016/j.tcs.2003.11.020.
  17. Greg Restall. Substructural Logics. In Edward N. Zalta and Uri Nodelman, editors, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Fall 2024 edition, 2024. Google Scholar
  18. 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.
  19. 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.
  20. P.D. Seymour and R. Thomas. Graph searching and a min-max theorem for tree-width. Journal of Combinatorial Theory, Series B, 58(1):22-33, 1993. URL: https://doi.org/10.1006/jctb.1993.1027.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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