Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.41974

Model Checking for Metric Extensions of Monadic Second-Order Logic

Dibyayan Chakraborty·Sebastian Ordyniak·Sebastian Siebertz
View original source ↗Read source document ↗Export metadata ↓

Abstract

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.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Dibyayan Chakraborty, Sebastian Ordyniak, Sebastian Siebertz. 2026-10-30. Model Checking for Metric Extensions of Monadic Second-Order Logic. https://arxiv.org/abs/2610.41974

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Formalizing Hyperspaces and Operations on Subsets of Polish Spaces over Abstract Exact Real Numbers

Building on our prior work on axiomatization of exact real computation by formalizing nondeterministic first-order partial computations over real and complex numbers in a constructive dependent type theory, we present a framework for certified computation on hyperspaces of subsets by formalizing various higher-order data types and operations. We first define open, closed, compact and overt subsets for generic spaces in an abstract topological way that allows short and elegant proofs with computational content coinciding with standard definitions in computable analysis and constructive mathematics. From these proofs we can extract programs for testing inclusion, overlapping of sets, et cetera. To enhance the efficiency of the extracted programs, we then focus on Polish spaces, where we give more efficient encodings based on metric properties of the space. As various computational properties depend on the continuity of the encoding functions, we introduce a nondeterministic version of a continuity principle which is natural in our formalization and valid under the standard type-2 realizability interpretation. Using this principle we further derive the computational equivalence between the generic and the metric encodings. Our theory is fully implemented in the Coq proof assistant. From proofs in this Coq formalization, we can extract certified programs for error-free operations on subsets. As an application, we provide a function that constructs fractals in Euclidean space, such as the Sierpinski triangle, from iterated function systems using the limit operation. The resulting programs can be used to draw such fractals up to any desired resolution.

cs.LO↗
arXiv2026

A Mimamsa Inspired Framework For Instruction Sequencing In AI Agents

This paper presents a formal framework for sequencing instructions in AI agents, inspired by the Indian philosophical system of Mimamsa. The framework formalizes sequencing mechanisms through action object pairs in three distinct ways: direct assertion (Srutikrama) for temporal precedence, purpose driven sequencing (Arthakrama) for functional dependencies, and iterative procedures (Pravrittikrama) for distinguishing between parallel and sequential execution in repetitive tasks. It introduces the syntax and semantics of an action object imperative logic, extending the MIRA formalism (Srinivasan and Parthasarathi, 2021) with explicit deduction rules for sequencing. The correctness of instruction sequencing is established through a validated theorem, which is based on object dependencies across successive instructions. This is further supported by proofs of soundness and completeness. This formal verification enables reliable instruction sequencing, impacting AI applications across areas like task planning and robotics by addressing temporal reasoning and dependency modeling.

cs.LO↗
arXiv2026

MathlibPR: Pull Request Merge-Outcome Benchmark for Formal Mathematical Libraries

The ecosystem of Lean and Mathlib has become the de facto standard for large language model (LLM) assisted formal reasoning with remarkable successes in recent years. Those successes, however, only consume Mathlib as an essential dependency but do not directly contribute to it. In the meantime, the growth of Mathlib has recently been bottlenecked by the review process, which requires human reviewers to judge whether proposed pull requests (PRs) follow the Mathlib's conventions and are worth integrating as part of a shared mathematical infrastructure. This leads to our central question: can LLMs help review Mathlib PRs? To this end, we introduce MathlibPR, a benchmark built from real Mathlib4 PR histories. We further propose a staged evaluation protocol and use it to evaluate both LLM models (e.g., DeepSeek, Qwen, Goedel, and Kimina) and LLM agents (e.g., Codex and Claude Code). Surprisingly, both LLM models and LLM agents struggle to distinguish merge-ready PRs from build-passing PRs that were revised or never merged. By turning Mathlib PR histories into a supervised signal, MathlibPR provides a step toward reviewer assistants and reward models that could help evaluate PRs and steer LLMs toward producing merge-ready Mathlib contributions.

cs.LO↗