# Monadic Decomposability of Regular Relations

## TL;DR

This paper investigates the problem of recognizing whether a regular relation can be decomposed into monadic formulas, establishing the precise computational complexity for DFA and NFA representations using novel techniques from infinite Ramsey theory.

## Contribution

It fully determines the complexity of deciding monadic decomposability of regular relations, resolving an open problem with new theoretical methods.

## Key findings

- NLOGSPACE-complete for DFA representations
- PSPACE-complete for NFA representations
- Decidability of recognizing monadic decomposability

## Abstract

Monadic decomposibility --- 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 a decision procedure for a given logical theory. In this paper, we revisit a classical decision problem in automata theory: given a regular (a.k.a. synchronized rational) relation, determine whether it is recognizable, i.e., it has a monadic decomposition (that is, a representation as a boolean combination of cartesian products of regular languages). Regular relations are expressive formalisms which, using an appropriate string encoding, can capture relations definable in Presburger Arithmetic. In fact, their expressive power coincide with relations definable in a universal automatic structure; equivalently, those definable by finite set interpretations in WS1S (Weak Second Order Theory of One Successor). Determining whether a regular relation admits a recognizable relation was known to be decidable (and in exponential time for binary relations), but its precise complexity still hitherto remains open. Our main contribution is to fully settle the complexity of this decision problem by developing new techniques employing infinite Ramsey theory. The complexity for DFA (resp. NFA) representations of regular relations is shown to be NLOGSPACE-complete (resp. \PSPACE-complete).