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

TL;DR

This paper develops logical and expression-based frameworks that precisely characterize the languages recognized by nondeterministic register automata with guessing over infinite alphabets, unifying automata, logic, and regular expressions.

Contribution

It introduces Scoped MSO logic with a segment modality and syntactic restrictions, and Data-Regular Expressions, establishing their equivalence to register automata over data domains.

Findings

Scoped MSO is expressively equivalent to NRA where strong guessing is eliminated.

Data-Regular Expressions are equivalent to NRA over arbitrary structures.

The formalisms provide a comprehensive descriptive theory for register automata.

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.