Scoped MSO, Register Automata, and Expressions: Equivalence over Data Words
Rados{\l}aw Pi\'orkowski

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 -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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · semigroups and automata theory · Logic, programming, and type systems
