Decidability Results for the Boundedness Problem

TL;DR

This paper establishes the decidability of the boundedness problem for monadic fixed-point recursion based on MSO formulas over trees, extending to structures of fixed finite tree-width and fragments of first-order logic.

Contribution

It proves the decidability of the boundedness problem for monadic fixed-point recursion on trees and other structures, using automata-theoretic and model-theoretic techniques, and determines its exact complexity.

Findings

Decidability of boundedness for MSO-based fixed-point recursion over trees.

Extension of decidability results to structures with fixed finite tree-width.

Derivation of known and new decidability results for fragments of first-order logic.

Abstract

We prove decidability of the boundedness problem for monadic least fixed-point recursion based on positive monadic second-order (MSO) formulae over trees. Given an MSO-formula phi(X,x) that is positive in X, it is decidable whether the fixed-point recursion based on phi is spurious over the class of all trees in the sense that there is some uniform finite bound for the number of iterations phi takes to reach its least fixed point, uniformly across all trees. We also identify the exact complexity of this problem. The proof uses automata-theoretic techniques. This key result extends, by means of model-theoretic interpretations, to show decidability of the boundedness problem for MSO and guarded second-order logic (GSO) over the classes of structures of fixed finite tree-width. Further model-theoretic transfer arguments allow us to derive major known decidability results for boundedness for fragments of first-order logic as well as new ones.