We show how membership in dasses of graphs definable in monadic second order logic and of bounded treewidth can be decided by finite sets of terminating reduction rules. The method is constructive in the sense that we describe an algorithm which will produce, from a formula in monadic second order logic and an integer k such that the class defined by the formula is of treewidth ≤ k, a set of rewrite rules that reduces any member of the class to one of finitely many graphs, in a number of steps bounded by the size of the graph. This reduction system corresponds to an algorithm that runs in time linear in the size of the graph.
CITATION STYLE
Arnborg, S., Courcelle, B., Proskurowski, A., & Seese, D. (1991). An algebraic theory of graph reduction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 532 LNCS, pp. 70–83). Springer Verlag. https://doi.org/10.1007/BFb0017382
Mendeley helps you to discover research relevant for your work.