Monadic second-order model-checking on decomposable matroids

TL;DR

This paper proves polynomial-time model-checking of monadic second-order logic on certain classes of matroids with bounded branch-width, simplifying previous proofs and extending to non-representable matroids.

Contribution

It provides a simpler proof for model-checking on representable matroids and introduces a new class of non-representable matroids with linear-time model-checking.

Findings

Polynomial-time model-checking on representable matroids of bounded branch-width.

Simplified proof approach using reduction to tree formulas.

New class of non-representable matroids with linear-time model-checking.

Abstract

A notion of branch-width, which generalizes the one known for graphs, can be defined for matroids. We first give a proof of the polynomial time model-checking of monadic second-order formulas on representable matroids of bounded branch-width, by reduction to monadic second-order formulas on trees. This proof is much simpler than the one previously known. We also provide a link between our logical approach and a grammar that allows to build matroids of bounded branch-width. Finally, we introduce a new class of non-necessarily representable matroids, described by a grammar and on which monadic second-order formulas can be checked in linear time.