@inproceedings{efa79372b2db4d25a4f92f58cef9b946,
title = "Brief Announcement: Distributed Model Checking on Graphs of Bounded Treedepth",
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.",
keywords = "congest, model checking, monadic second order logic, treedepth",
author = "Fomin, \{Fedor V.\} and Pierre Fraigniaud and Pedro Montealegre and Ivan Rapaport and Ioan Todinca",
note = "Publisher Copyright: {\textcopyright} 2024 Copyright is held by the owner/author(s). Publication rights licensed to ACM.; 43rd ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, PODC 2024 ; Conference date: 17-06-2024 Through 21-06-2024",
year = "2024",
month = jun,
day = "17",
doi = "10.1145/3662158.3662793",
language = "English",
series = "Proceedings of the Annual ACM Symposium on Principles of Distributed Computing",
publisher = "Association for Computing Machinery",
pages = "205--208",
booktitle = "PODC 2024 - Proceedings of the 2024 ACM Symposium on Principles of Distributed Computing",
}