2009/04/13 by Stéphane Grumbach, Stephane Grumbach, Grumbach, Stephane +2
Computer Science · #Distributed #Distributed systems and fault tolerance #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Parallel #Software Testing and Debugging Techniques #and Cluster Computing (cs.DC) #cs.DC #cs.LO
paper · pdf · doi:10.48550/arxiv.0904.1902
30 pages, 4 figures, llncs.cls,llncsdoc.sty
arxiv created 2009/04/13 · openalex publication_date 2009/04/13 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We consider distributed model-checking of Monadic Second-Order logic (MSO) on graphs which constitute the topology of communication networks. The graph is thus both the structure being checked and the system on which the distributed computation is performed. We prove that MSO can be distributively model-checked with only a constant number of messages sent over each link for planar networks with bounded diameter, as well as for networks with bounded degree and bounded tree-length. The distributed algorithms rely on nontrivial transformations of linear time sequential algorithms for tree decompositions of bounded tree-width graphs.