Scoped MSO, Register Automata, and Expressions: Equivalence over Data Words

Abstract

This paper establishes logical and expression-based characterizations for the class of languages recognized by nondeterministic register automata with guessing (NRA) over infinite alphabets. We introduce Scoped MSO, a logic featuring a novel segment modality and syntactic restrictions on data comparisons. We prove this logic is expressively equivalent to NRA over data domains where ``strong guessing'' can be eliminated. Furthermore, we define Data-Regular Expressions, a minimalist regular-expression calculus built from quantifier-free regions and equipped with $k$-contracting concatenation, and demonstrate its equivalence to NRA over arbitrary relational structures. Together, these formalisms provide a robust descriptive theory for register automata, bridging the gap between automata, logic, and expressions.