Abstract
Monadic decomposability — the ability to determine whether a formula in a given logical theory can be decomposed into a Boolean combination of monadic formulas — is a powerful tool for devising decision procedures. In this paper, we revisit a classical decision problem in automata theory: given a regular (synchronized rational) relation, determine whether it is recognizable, i.e., whether it admits a monadic decomposition as a Boolean combination of Cartesian products of regular languages. Regular relations are highly expressive and, under suitable encodings, capture relations definable in Presburger Arithmetic. Their expressive power coincides with relations definable in universal automatic structures, equivalently those definable by finite set interpretations in WS1S (Weak Second Order Theory of One Successor). While decidability of this problem was known (and exponential time for binary relations), its exact complexity remained open. Our main contribution is to fully settle the complexity of this decision problem by developing new techniques based on infinite Ramsey theory. We show that the problem is NLOGSPACE-complete for DFA representations and PSPACE-complete for NFA representations of regular relations.