zbMATH — the first resource for mathematics

Special tree-width and the verification of monadic second-order graph properties. (English) Zbl 1245.68133
Lodaya, Kamal (ed.) et al., IARCS annual conference on foundations of software technology and theoretical computer science (FSTTCS 2010), December 15–18, 2010, Chennai, India. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-23-1). LIPIcs – Leibniz International Proceedings in Informatics 8, 13-29, electronic only (2010).
Summary: 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.
For the entire collection see [Zbl 1213.68048].

68Q60 Specification and verification (program logics, model checking, etc.)
68R10 Graph theory (including graph drawing) in computer science
03B70 Logic in computer science
68Q45 Formal languages and automata
Full Text: DOI Link