2026-07-22T06:37:12Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2849 2024-03-06T10:33:36Z ddc:004 open_access

Special tree-width and the verification of monadic second-order graph pr operties Courcelle, Bruno model-checking monadic second-order logic fixed-parameter tractability special tree-width The model-checking problem for monadic second-order logic on graphs is fixed-parameter tractable with respect to tree-width and clique-width. The proof constructs finite deterministic automata from monadic second-order sentences, but this computation produces automata of hyper-exponential sizes, and this is not avoidable. To overcome this difficulty, we propose to consider particular monadic second-order graph properties that are nevertheless interesting for Graph Theory and to interpret automata instead of trying to compile them (joint work with I. Durand). For checking monadic second-order sentences written with edge set quantifications, the appropriate parameter is tree-width. We introduce special tree-width, a graph complexity measure between path-width and tree-width. The corresponding automata are easier to construct than those for tree-width. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Bruno Courcelle 2010 Is Part Of LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2010.13 urn:nbn:de:0030-drops-28494 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.13 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode