Alternating Nominal Automata with Name Allocation

TL;DR

This paper introduces regular alternating nominal automata (RANAs) that extend existing models with name allocation, demonstrating that their decision problems remain elementary in complexity even with unbounded registers, and improving model checking complexity.

Contribution

It extends automata models with alternation and name allocation, showing elementary complexity persists and enabling nearly complete de-alternation.

Findings

Elementary complexity for non-emptiness and inclusion problems.

Nearly complete de-alternation up to a deadlocked universal state.

Improved complexity bounds for model checking Bar-μTL.

Abstract

Formal languages over infinite alphabets serve as abstractions of structures and processes carrying data. Automata models over infinite alphabets, such as classical register automata or, equivalently, nominal orbit-finite automata, tend to have computationally hard or even undecidable reasoning problems unless stringent restrictions are imposed on either the power of control or the number of registers. This has been shown to be ameliorated in automata models with name allocation such as regular nondeterministic nominal automata, which allow for deciding language inclusion in elementary complexity even with unboundedly many registers while retaining a reasonable level of expressiveness. In the present work, we demonstrate that elementary complexity survives under extending the power of control to alternation: We introduce regular alternating nominal automata (RANAs), and show that their non-emptiness and inclusion problems have elementary complexity even when the number of registers is unbounded. Moreover, we show that RANAs allow for nearly complete de-alternation, specifically de-alternation up to a single deadlocked universal state. As a corollary to our results, we improve the complexity of model checking for a flavour of Bar-$\mu$TL, a fixed-point logic with name allocation over finite data words, by one exponential level.