Nominal Tree Automata With Name Allocation
Simon Prucker, Lutz Schröder
TL;DR
This work introduces Regular Nominal Tree Automata (RNTA), a model for data-tree languages that integrates name allocation within nominal sets to support unbounded nondeterminism and unbounded registers. By leveraging alpha-equivalence and a name-dropping modification, the authors achieve inclusion checking in elementary (parametrized exponential) time, specifically doubly exponential, even with unbounded registers. The core technique reduces the data-tree inclusion problem to finite NFTA inclusion over a carefully bounded name set, enabling practical reasoning about alphatic data trees under global, branchwise, or local freshness semantics. The approach supports languages arising from binding constructs (e.g., XML-like data, lambda- and pi-calculus fragments) and paves the way for extensions to infinite trees and coalgebraic frameworks.
Abstract
Data trees serve as an abstraction of structured data, such as XML documents. A number of specification formalisms for languages of data trees have been developed, many of them adhering to the paradigm of register automata, which is based on storing data values encountered on the tree in registers for subsequent comparison with further data values. Already on word languages, the expressiveness of such automata models typically increases with the power of control (e.g. deterministic, non-deterministic, alternating). Language inclusion is typically undecidable for non-deterministic or alternating models unless the number of registers is radically restricted, and even then often remains non-elementary. We present an automaton model for data trees that retains a reasonable level of expressiveness, in particular allows non-determinism and any number of registers, while admitting language inclusion checking in elementary complexity, in fact in parametrized exponential time. We phrase the description of our automaton model in the language of nominal sets, building on the recently introduced paradigm of explicit name allocation in nominal automata.