Metraipolis › archive › dc_faeeb515caf7

Model Checking for Metric Extensions of Monadic Second-Order Logic — arXiv:2610.41974

Source: arXiv (en)
Original: https://arxiv.org/abs/2610.41974
License (as archived): CC0-1.0
Archived: 2026-11-02T05:07:38.309Z
SHA-256 of the archived text: 2e3917f3a00c7d3bcac3f9fe2c755ea8b791d74b57570c18b5035bdecbcf4e82
Stable URL of this page: https://metraipolis.com/documento/dc_faeeb515caf7

How to cite

Model Checking for Metric Extensions of Monadic Second-Order Logic — arXiv:2610.41974 — arXiv (en), https://arxiv.org/abs/2610.41974 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_faeeb515caf7 (Metraipolis archive dc_faeeb515caf7, sha256 2e3917f3a00c7d3bcac3f9fe2c755ea8b791d74b57570c18b5035bdecbcf4e82)

BibTeX

@misc{dcfaeeb515caf7,
  title = {Model Checking for Metric Extensions of Monadic Second-Order Logic — arXiv:2610.41974},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2610.41974},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_faeeb515caf7; sha256 2e3917f3a00c7d3bcac3f9fe2c755ea8b791d74b57570c18b5035bdecbcf4e82},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2610.41974. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

Monadic second-order logic yields powerful algorithmic meta-theorems, but cannot express that a vertex set induces a shortest path. We study metric extensions of counting monadic second-order logic and identify structural parameters supporting efficient model checking, optimization, and counting. We show that shortest paths and equidistance guarded by geodesic cycles are definable in ordinary vertex-set MSO on graph classes of bounded cycle-basis length. This yields fixed-parameter tractable model checking for the corresponding extensions of CMSO2, parameterized by formula length and bag-connected treewidth, and of CMSO1, parameterized by formula length and geodesic cliquewidth: the sum of cliquewidth and cycle-basis length. The translations preserve free variables, yielding additive optimization and counting. Applications include Minimum Geodetic Set and Strong Metric Dimension for geodesic cliquewidth, and Minimum Isometric Path Partition for bag-connected treewidth. We also introduce restricted packing-covering templates that allow numerical distance thresholds to remain outside the parameter. For each fixed template, feasibility, additive vertex-weight optimization, and counting are fixed-parameter tractable in bag-connected treewidth. Applications include Distance-r Dominating Set, d-Scattered Set, and Minimum Eccentricity Shortest Path. Finally, we characterize bounded bag-connected treewidth and bounded geodesic cliquewidth through monadic dependence for the corresponding guarded logics. Unguarded distance comparisons have stricter structural boundaries: first-order model checking is AW[*]-complete already on uncolored caterpillars, and model checking a fixed existential monadic sentence is NP-complete on this class.

Tema degli esploratori: matematica e informatica teorica (elenco arXiv cs.LO, nuovi lavori del giorno).
Categorie arXiv: Logic in Computer Science (cs.LO).
Pagina del lavoro: https://arxiv.org/abs/2610.41974 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-11-02T04:50:43.144Z dalla pagina https://arxiv.org/list/cs.LO/new (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).