Special tree-width and the verification of monadic second-order graph pr operties

Courcelle, Bruno

doi:10.4230/LIPIcs.FSTTCS.2010.13

Document

Special tree-width and the verification of monadic second-order graph pr operties

Author Bruno Courcelle

Part of: Volume: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2010-12-14

PDF

File

PDF

LIPIcs.FSTTCS.2010.13.pdf

Filesize: 0.49 MB
17 pages

Document Identifiers

DOI: 10.4230/LIPIcs.FSTTCS.2010.13
URN: urn:nbn:de:0030-drops-28494

Subject Classification

Keywords

model-checking
monadic second-order logic
fixed-parameter tractability
special tree-width

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

Abstract

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.

Cite As Get BibTex

Bruno Courcelle. Special tree-width and the verification of monadic second-order graph pr operties. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 13-29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010) https://doi.org/10.4230/LIPIcs.FSTTCS.2010.13

Author Details

Bruno Courcelle

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail