Nominal Tree Automata With Name Allocation

TL;DR

This paper introduces a new automaton model for data trees that supports non-determinism and multiple registers, enabling decidable language inclusion checks within elementary complexity using nominal sets and explicit name allocation.

Contribution

It proposes a novel nominal automaton model for data trees that balances expressiveness with decidability of language inclusion.

Findings

Supports non-determinism and any number of registers

Allows language inclusion checking in parametrized exponential time

Uses nominal sets and explicit name allocation

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.