Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Radosław Piórkowski

TL;DR

This work develops a unified descriptive theory for data-word languages by introducing Data-Regular Expressions and Scoped MSO as minimalist yet expressive formalisms that match the capabilities of nondeterministic register automata with guessing ($\mathrm{NRA}^{\mathrm{g}}$). It proves expressive equivalences: $\mathcal{L}(\mathrm{DRE})=\mathcal{L}(\mathrm{NRA}^{\mathrm{g}})$ and $\mathcal{L}(\mathrm{MSO}_{\mathrm{S}}[<,\Sigma,\bA])=\mathcal{L}(\mathrm{NRA}^{\mathrm{g}})$ under atoms that admit elimination of strong guessing, with extensions to infinite words and arbitrary relational structures via contraction-based encodings. The new formalisms provide a robust bridge among automata, logic, and expressions for data words, enabling decidability results and new avenues for addressing open questions such as separability and expressive boundaries. The framework supports systematic translations in both directions between these descriptions and lays groundwork for tackling broader data-language hierarchies.

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.

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

TL;DR

This work develops a unified descriptive theory for data-word languages by introducing Data-Regular Expressions and Scoped MSO as minimalist yet expressive formalisms that match the capabilities of nondeterministic register automata with guessing (). It proves expressive equivalences: and under atoms that admit elimination of strong guessing, with extensions to infinite words and arbitrary relational structures via contraction-based encodings. The new formalisms provide a robust bridge among automata, logic, and expressions for data words, enabling decidability results and new avenues for addressing open questions such as separability and expressive boundaries. The framework supports systematic translations in both directions between these descriptions and lays groundwork for tackling broader data-language hierarchies.

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.
Paper Structure (22 sections, 18 theorems, 28 equations, 2 figures)

This paper contains 22 sections, 18 theorems, 28 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Formalisms for regular languages
  4. Words over infinite alphabets
  5. Register automata---a formalism for data word languages
  6. New formalisms equivalent to register automata
  7. Data regular expressions
  8. Scoped MSO
  9. Proofs of main theorems
  10. Expressions vs. automata
  11. Logic vs. automata
  12. Extensions and special cases
  13. Infinite words
  14. Atoms requiring strong guessing
  15. NRA without guessing
  16. ...and 7 more sections

Key Result

Theorem 1

$\operatorname{ \cL } \mathopen{}\bracketInner*{ { \mathrm{NFA} } \squareBracketInner*{\Sigma}\xspace} = \operatorname{ \cL } \mathopen{}\bracketInner*{ { \mathrm{RE} } \squa

Figures (2)

  • Figure 1: Formation of operating intervals for each of four types for two registers $\setInner*{r, s}$.
  • Figure 2: Correspondence between a run $\pi$ of $\cA$ performing strong guesses and a run $\pi'$ of $\cB$ with only weak guesses.

Theorems & Definitions (27)

  • Theorem 1: Kleene kleene1956representation
  • Theorem 2: Büchi, Elgot, Trakhtenbrot Buchi-mso-automataelgot1961decisionzbMATH03186871
  • Example 3
  • Definition 4: Elimination of strong guessing.
  • Theorem 5
  • Example 7
  • Example 8
  • Theorem 9
  • Corollary 10
  • Lemma 11
  • ...and 17 more