Document Open Access Logo

Distributed Model Checking on Graphs of Bounded Treedepth

Authors Fedor V. Fomin , Pierre Fraigniaud , Pedro Montealegre , Ivan Rapaport , Ioan Todinca

PDF
Thumbnail PDF

File

LIPIcs.DISC.2024.25.pdf
  • Filesize: 0.95 MB
  • 20 pages

Document Identifiers

Author Details

Fedor V. Fomin
  • University of Bergen, Norway
Pierre Fraigniaud
  • IRIF, Université Paris Cité and CNRS, Paris, France
Pedro Montealegre
  • Universidad Adolfo Ibañez, Santiago, Chile
Ivan Rapaport
  • Universidad de Chile, Santiago, Chile
Ioan Todinca
  • LIFO, Université d'Orléans, France
  • INSA Centre-Val de Loire, Orléans, France

Funding

  • Fomin, Fedor V.: the research leading to these results has received funding from the Research Council of Norway via the project BWCA (grant no. 314528).
  • Fraigniaud, Pierre: partially supported by the ANR projects DUCAT (ANR-20-CE48-0006), and QuData (ANR-18-CE47-0010).
  • Montealegre, Pedro: P.M. has received funding from FONDECYT 1230599.
  • Rapaport, Ivan: I.R. has received funding from FB210005, BASAL funds for centers of excellence from ANID- Chile, and FONDECYT 1220142.

Cite As Get BibTex

Fedor V. Fomin, Pierre Fraigniaud, Pedro Montealegre, Ivan Rapaport, and Ioan Todinca. Distributed Model Checking on Graphs of Bounded Treedepth. In 38th International Symposium on Distributed Computing (DISC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 319, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.DISC.2024.25

Abstract

We establish that every monadic second-order logic (MSO) formula on graphs with bounded treedepth is decidable in a constant number of rounds within the CONGEST model. To our knowledge, this marks the first meta-theorem regarding distributed model-checking. Various optimization problems on graphs are expressible in MSO. Examples include determining whether a graph G has a clique of size k, whether it admits a coloring with k colors, whether it contains a graph H as a subgraph or minor, or whether terminal vertices in G could be connected via vertex-disjoint paths. Our meta-theorem significantly enhances the work of Bousquet et al. [PODC 2022], which was focused on distributed certification of MSO on graphs with bounded treedepth. Moreover, our results can be extended to solving optimization and counting problems expressible in MSO, in graphs of bounded treedepth.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed algorithms
  • Theory of computation → Verification by model checking
Keywords
  • proof-labeling schemes
  • local computing
  • CONGEST model

Metrics

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

Related Versions

References

  1. Alkida Balliu, Gianlorenzo D'Angelo, Pierre Fraigniaud, and Dennis Olivetti. What can be verified locally? J. Comput. Syst. Sci., 97:106-120, 2018. URL: https://doi.org/10.1016/J.JCSS.2018.05.004.
  2. Aviv Bick, Gillat Kol, and Rotem Oshman. Distributed zero-knowledge proofs over networks. In 33rd ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 2426-2458, 2022. URL: https://doi.org/10.1137/1.9781611977073.97.
  3. Lélia Blin, Laurent Feuilloley, and Gabriel Le Bouder. Optimal space lower bound for deterministic self-stabilizing leader election algorithms. Discret. Math. Theor. Comput. Sci., 25:1-17, 2023. URL: https://doi.org/10.46298/DMTCS.9335.
  4. Hans L. Bodlaender. A partial k-arboretum of graphs with bounded treewidth. Theoretical Computer Science, 209(1-2):1-45, 1998. URL: https://doi.org/10.1016/S0304-3975(97)00228-4.
  5. Richard B. Borie, R. Gary Parker, and Craig A. Tovey. Automatic generation of linear-time algorithms from predicate calculus descriptions of problems on recursively constructed graph families. Algorithmica, 7(5&6):555-581, 1992. URL: https://doi.org/10.1007/BF01758777.
  6. Nicolas Bousquet, Laurent Feuilloley, and Théo Pierron. Local certification of graph decompositions and applications to minor-free classes. In 25th International Conference on Principles of Distributed Systems (OPODIS), volume 217 of LIPIcs, pages 22:1-22:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.OPODIS.2021.22.
  7. Keren Censor-Hillel, Mohsen Ghaffari, and Fabian Kuhn. Distributed connectivity decomposition. In Proceedings of the 2014 ACM symposium on Principles of distributed computing, pages 156-165, 2014. URL: https://doi.org/10.1145/2611462.2611491.
  8. Keren Censor-Hillel, Ami Paz, and Mor Perry. Approximate proof-labeling schemes. Theor. Comput. Sci., 811:112-124, 2020. URL: https://doi.org/10.1016/J.TCS.2018.08.020.
  9. Yi-Jun Chang. Efficient distributed decomposition and routing algorithms in minor-free networks and their applications. In Proceedings of the 2023 ACM Symposium on Principles of Distributed Computing, pages 55-66, 2023. URL: https://doi.org/10.1145/3583668.3594604.
  10. Bruno Courcelle. The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf. Comput., 85(1):12-75, 1990. URL: https://doi.org/10.1016/0890-5401(90)90043-H.
  11. Pierluigi Crescenzi, Pierre Fraigniaud, and Ami Paz. Trade-offs in distributed interactive proofs. In 33rd International Symposium on Distributed Computing (DISC), volume 146 of LIPIcs, pages 13:1-13:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPICS.DISC.2019.13.
  12. Atish Das Sarma, Stephan Holzer, Liah Kor, Amos Korman, Danupon Nanongkai, Gopal Pandurangan, David Peleg, and Roger Wattenhofer. Distributed verification and hardness of distributed approximation. SIAM J. Comput., 41(5):1235-1265, 2012. URL: https://doi.org/10.1137/11085178X.
  13. Andrew Drucker, Fabian Kuhn, and Rotem Oshman. On the power of the congested clique model. In 33rd ACM Symposium on Principles of Distributed Computing (PODC), pages 367-376, 2014. URL: https://doi.org/10.1145/2611462.2611493.
  14. Michael Elberfeld, Martin Grohe, and Till Tantau. Where first-order and monadic second-order logic coincide. ACM Trans. Comput. Log., 17(4):25, 2016. URL: https://doi.org/10.1145/2946799.
  15. Gábor Elek. Planarity can be verified by an approximate proof labeling scheme in constant-time. J. Comb. Theory, Ser. A, 191:105643, 2022. URL: https://doi.org/10.1016/J.JCTA.2022.105643.
  16. Yuval Emek, Yuval Gil, and Shay Kutten. Locally restricted proof labeling schemes. In 36th International Symposium on Distributed Computing (DISC), volume 246 of LIPIcs, pages 20:1-20:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.DISC.2022.20.
  17. Louis Esperet and Benjamin Lévêque. Local certification of graphs on surfaces. Theor. Comput. Sci., 909:68-75, 2022. URL: https://doi.org/10.1016/J.TCS.2022.01.023.
  18. Louis Esperet and Sergey Norin. Testability and local certification of monotone properties in minor-closed classes. In 49th International Colloquium on Automata, Languages, and Programming (ICALP), volume 229 of LIPIcs, pages 58:1-58:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.ICALP.2022.58.
  19. Laurent Feuilloley. Introduction to local certification. Discret. Math. Theor. Comput. Sci., 23(3):1-23, 2021. URL: https://doi.org/10.46298/DMTCS.6280.
  20. Laurent Feuilloley, Nicolas Bousquet, and Théo Pierron. What can be certified compactly? compact local certification of MSO properties in tree-like graphs. In 41st ACM Symposium on Principles of Distributed Computing (PODC), pages 131-140, 2022. URL: https://doi.org/10.1145/3519270.3538416.
  21. Laurent Feuilloley and Pierre Fraigniaud. Survey of distributed decision. Bull. EATCS, 119, 2016. URL: http://eatcs.org/beatcs/index.php/beatcs/article/view/411.
  22. Laurent Feuilloley and Pierre Fraigniaud. Error-sensitive proof-labeling schemes. J. Parallel Distributed Comput., 166:149-165, 2022. URL: https://doi.org/10.1016/J.JPDC.2022.04.015.
  23. Laurent Feuilloley, Pierre Fraigniaud, and Juho Hirvonen. A hierarchy of local decision. Theor. Comput. Sci., 856:51-67, 2021. URL: https://doi.org/10.1016/J.TCS.2020.12.017.
  24. Laurent Feuilloley, Pierre Fraigniaud, Juho Hirvonen, Ami Paz, and Mor Perry. Redundancy in distributed proofs. Distributed Comput., 34(2):113-132, 2021. URL: https://doi.org/10.1007/S00446-020-00386-Z.
  25. Laurent Feuilloley, Pierre Fraigniaud, Pedro Montealegre, Ivan Rapaport, Éric Rémila, and Ioan Todinca. Compact distributed certification of planar graphs. Algorithmica, 83(7):2215-2244, 2021. URL: https://doi.org/10.1007/S00453-021-00823-W.
  26. Laurent Feuilloley, Pierre Fraigniaud, Pedro Montealegre, Ivan Rapaport, Éric Rémila, and Ioan Todinca. Local certification of graphs with bounded genus. Discret. Appl. Math., 325:9-36, 2023. URL: https://doi.org/10.1016/J.DAM.2022.10.004.
  27. Orr Fischer, Tzlil Gonen, Fabian Kuhn, and Rotem Oshman. Possibilities and impossibilities for distributed subgraph detection. In Christian Scheideler and Jeremy T. Fineman, editors, Proceedings of the 30th on Symposium on Parallelism in Algorithms and Architectures, SPAA 2018, Vienna, Austria, July 16-18, 2018, pages 153-162. ACM, 2018. URL: https://doi.org/10.1145/3210377.3210401.
  28. Fedor V. Fomin, Pierre Fraigniaud, Pedro Montealegre, Ivan Rapaport, and Ioan Todinca. Distributed model checking on graphs of bounded treedepth. CoRR, abs/2405.03321, 2024. URL: https://doi.org/10.48550/arXiv.2405.03321.
  29. Pierre Fraigniaud, François Le Gall, Harumichi Nishimura, and Ami Paz. Distributed quantum proofs for replicated data. In 12th Innovations in Theoretical Computer Science Conference (ITCS), volume 185 of LIPIcs, pages 28:1-28:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.ITCS.2021.28.
  30. Pierre Fraigniaud, Mika Göös, Amos Korman, Merav Parter, and David Peleg. Randomized distributed decision. Distributed Comput., 27(6):419-434, 2014. URL: https://doi.org/10.1007/S00446-014-0211-X.
  31. Pierre Fraigniaud, Mika Göös, Amos Korman, and Jukka Suomela. What can be decided locally without identifiers? In 32nd ACM Symposium on Principles of Distributed Computing (PODC), pages 157-165, 2013. URL: https://doi.org/10.1145/2484239.2484264.
  32. Pierre Fraigniaud, Amos Korman, and David Peleg. Towards a complexity theory for local distributed computing. J. ACM, 60(5):35:1-35:26, 2013. URL: https://doi.org/10.1145/2499228.
  33. Pierre Fraigniaud, Frédéric Mazoit, Pedro Montealegre, Ivan Rapaport, and Ioan Todinca. Distributed certification for classes of dense graphs. In 37th International Symposium on Distributed Computing (DISC), volume 281 of LIPIcs, pages 20:1-20:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.DISC.2023.20.
  34. Pierre Fraigniaud, Pedro Montealegre, Ivan Rapaport, and Ioan Todinca. A meta-theorem for distributed certification. Algorithmica, 86(2):585-612, 2024. URL: https://doi.org/10.1007/S00453-023-01185-1.
  35. Pierre Fraigniaud, Boaz Patt-Shamir, and Mor Perry. Randomized proof-labeling schemes. Distributed Comput., 32(3):217-234, 2019. URL: https://doi.org/10.1007/S00446-018-0340-8.
  36. Jakub Gajarský and Petr Hlinený. Kernelizing MSO properties of trees of fixed height, and some consequences. Log. Methods Comput. Sci., 11(1):1-26, 2015. URL: https://doi.org/10.2168/LMCS-11(1:19)2015.
  37. François Le Gall, Masayuki Miyamoto, and Harumichi Nishimura. Distributed quantum interactive proofs. In 40th International Symposium on Theoretical Aspects of Computer Science (STACS), volume 254 of LIPIcs, pages 42:1-42:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.STACS.2023.42.
  38. JA Garay, S Kutten, and D Peleg. A sub-linear time distributed algorithm for minimum-weight spanning trees. In Proceedings of 1993 IEEE 34th Annual Foundations of Computer Science, pages 659-668. IEEE, 1993. Google Scholar
  39. Mohsen Ghaffari, Andreas Karrenbauer, Fabian Kuhn, Christoph Lenzen, and Boaz Patt-Shamir. Near-optimal distributed maximum flow. In Proceedings of the 2015 ACM Symposium on Principles of Distributed Computing, pages 81-90, 2015. Google Scholar
  40. Mohsen Ghaffari and Fabian Kuhn. Distributed minimum cut approximation. In International Symposium on Distributed Computing, pages 1-15. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-41527-2_1.
  41. Mohsen Ghaffari and Christoph Lenzen. Near-optimal distributed tree embedding. In International Symposium on Distributed Computing, pages 197-211. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-45174-8_14.
  42. Mohsen Ghaffari and Merav Parter. Near-optimal distributed dfs in planar graphs. In 31st International Symposium on Distributed Computing (DISC 2017), pages 21:1-21:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPICS.DISC.2017.21.
  43. Mika Göös and Jukka Suomela. Locally checkable proofs in distributed computing. Theory Comput., 12(1):1-33, 2016. URL: https://doi.org/10.4086/TOC.2016.V012A019.
  44. Martin Grohe. Logic, graphs, and algorithms. In Logic and Automata: History and Perspectives, in Honor of Wolfgang Thomas, volume 2 of Texts in Logic and Games, pages 357-422. Amsterdam University Press, 2008. URL: https://eccc.weizmann.ac.il/report/2007/091/.
  45. Martin Grohe and Stephan Kreutzer. Methods for algorithmic meta theorems. In Model Theoretic Methods in Finite Combinatorics - AMS-ASL Joint Special Session, volume 558, pages 181-206. AMS, 2009. URL: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.395.8282&rep=rep1&type=pdf.
  46. Bernhard Haeupler, Taisuke Izumi, and Goran Zuzic. Low-congestion shortcuts without embedding. In Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing, pages 451-460, 2016. URL: https://doi.org/10.1145/2933057.2933112.
  47. Monika Henzinger, Sebastian Krinninger, and Danupon Nanongkai. A deterministic almost-tight distributed algorithm for approximating single-source shortest paths. In Proceedings of the forty-eighth annual ACM symposium on Theory of Computing, pages 489-498, 2016. URL: https://doi.org/10.1145/2897518.2897638.
  48. Juho Hirvonen and Jukka Suomela. Distributed Algorithms 2020. Aalto University, 2020. URL: https://jukkasuomela.fi/da2020/.
  49. Gillat Kol, Rotem Oshman, and Raghuvansh R. Saxena. Interactive distributed proofs. In 37th ACM Symposium on Principles of Distributed Computing (PODC), pages 255-264. ACM, 2018. URL: https://dl.acm.org/citation.cfm?id=3212771.
  50. Amos Korman, Shay Kutten, and Toshimitsu Masuzawa. Fast and compact self-stabilizing verification, computation, and fault detection of an MST. Distributed Comput., 28(4):253-295, 2015. URL: https://doi.org/10.1007/S00446-015-0242-Y.
  51. Amos Korman, Shay Kutten, and David Peleg. Proof labeling schemes. Distributed Comput., 22(4):215-233, 2010. URL: https://doi.org/10.1007/S00446-010-0095-3.
  52. Stephan Kreutzer. Algorithmic meta-theorems. In Finite and Algorithmic Model Theory, volume 379 of London Mathematical Society Lecture Note Series, pages 177-270. Cambridge University Press, 2011. URL: http://www.cs.ox.ac.uk/people/stephan.kreutzer/Publications/amt-survey.pdf.
  53. Shay Kutten and David Peleg. Fast distributed construction of k-dominating sets and applications. In Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing, pages 238-251, 1995. Google Scholar
  54. Christoph Lenzen and Boaz Patt-Shamir. Improved distributed steiner forest construction. In Proceedings of the 2014 ACM symposium on Principles of distributed computing, pages 262-271, 2014. URL: https://doi.org/10.1145/2611462.2611464.
  55. Danupon Nanongkai. Distributed approximation algorithms for weighted shortest paths. In Proceedings of the forty-sixth annual ACM symposium on Theory of computing, pages 565-573, 2014. URL: https://doi.org/10.1145/2591796.2591850.
  56. Danupon Nanongkai and Hsin-Hao Su. Almost-tight distributed minimum cut algorithms. In International Symposium on Distributed Computing, pages 439-453. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-45174-8_30.
  57. Moni Naor, Merav Parter, and Eylon Yogev. The power of distributed verifiers in interactive proofs. In 31st ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 1096-115. SIAM, 2020. URL: https://doi.org/10.1137/1.9781611975994.67.
  58. Jaroslav Nešetřil and Patrice Ossona de Mendez. Sparsity - Graphs, Structures, and Algorithms, volume 28 of Algorithms and combinatorics. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-27875-4.
  59. Jaroslav Nešetřil and Patrice Ossona de Mendez. A distributed low tree-depth decomposition algorithm for bounded expansion classes. Distributed Comput., 29(1):39-49, 2016. URL: https://doi.org/10.1007/S00446-015-0251-X.
  60. David Peleg. Distributed computing: a locality-sensitive approach. SIAM, 2000. Google Scholar
  61. Neil Robertson and Paul D. Seymour. Graph minors. III. Planar tree-width. J. Comb. Theory, Ser. B, 36(1):49-64, 1984. URL: https://doi.org/10.1016/0095-8956(84)90013-3.
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