Kernelizing MSO properties of trees of fixed height, and some consequences

DOI10.2168/LMCS-11(1:19)2015MaRDI QIDQ5246725zbMATH OpenFDO

Authors Jakub Gajarský, Petr Hliněný

Publication date 22 April 2015

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1204.5194

zbMATH Keywords

algorithmic meta-theoremsCourcelle's theoremmodel checkingMSO logicshrub-depthtree-depth

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Automata and formal grammars in connection with logical questions (03D05) Trees (05C05) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Fix an integer h>=1. In the universe of coloured trees of height at most h, we prove that for any graph decision problem defined by an MSO formula with r quantifiers, there exists a set of kernels, each of size bounded by an elementary function of r and the number of colours. This yields two noteworthy consequences. Consider any graph class G having a one-dimensional MSO interpretation in the universe of coloured trees of height h (equivalently, G is a class of shrub-depth h). First, class G admits an MSO model checking algorithm whose runtime has an elementary dependence on the formula size. Second, on G the expressive powers of FO and MSO coincide (which extends a 2012 result of Elberfeld, Grohe, and Tantau).

Recommendations

• scientific article; zbMATH DE number 6678444
• When trees grow low: shrubs and fast \(\mathrm{MSO}_{1}\)
• Model checking lower bounds for simple graphs
• Tree-depth, quantifier elimination, and quantifier rank
• Model checking lower bounds for simple graphs

Cited in

(13)

• Tree-depth and vertex-minors
• When trees grow low: shrubs and fast \(\mathrm{MSO}_{1}\)
• scientific article; zbMATH DE number 6678444 (Why is no real title available?)
• scientific article; zbMATH DE number 7029306 (Why is no real title available?)
• Parameterized complexity of fair vertex evaluation problems
• Where first-order and monadic second-order logic coincide
• Extended MSO model checking via small vertex integrity
• On classes of bounded tree rank, their interpretations, and efficient sparsification
• Distributed model checking on graphs of bounded treedepth
• Elementary first-order model checking for sparse graphs
• Brief announcement: Distributed model checking on graphs of bounded treedepth
• Fine-grained meta-theorems for vertex integrity
• Characterization of the average tree solution and its kernel

This page was built for publication: Kernelizing MSO properties of trees of fixed height, and some consequences

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5246725)