
























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.
此内容由惯性聚合(RSS阅读器)自动聚合整理,仅供阅读参考。 原文来自 — 版权归原作者所有。