Alternating Nominal Automata with Name Allocation

Frank F, Hausmann D, Milius S, Schröder L, Urbat H (2025)

Publication Type: Conference contribution

Publication year: 2025

Journal

Proceedings - Symposium on Logic in Computer Science Institute of Electrical and Electronics Engineers

Publisher: Institute of Electrical and Electronics Engineers Inc.

Pages Range: 57-70

Conference Proceedings Title: Proceedings - Symposium on Logic in Computer Science

Event location: Singapore SG

ISBN: 9798331554644

DOI: 10.1109/LICS65433.2025.00012

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-μTL, a fixed-point logic with name allocation over finite data words, by one exponential level.

Authors with CRIS profile

Florian Frank Graduiertenkolleg 2475/2 - Cyberkriminalität und Forensische Informatik Stefan Milius Lehrstuhl für Informatik 8 (Theoretische Informatik) Lutz Schröder Lehrstuhl für Informatik 8 (Theoretische Informatik) Henning Urbat Lehrstuhl für Informatik 8 (Theoretische Informatik)

Involved external institutions

The University of Liverpool GB United Kingdom (GB)

How to cite

APA:

Frank, F., Hausmann, D., Milius, S., Schröder, L., & Urbat, H. (2025). Alternating Nominal Automata with Name Allocation. In Proceedings - Symposium on Logic in Computer Science (pp. 57-70). Singapore, SG: Institute of Electrical and Electronics Engineers Inc..

MLA:

Frank, Florian, et al. "Alternating Nominal Automata with Name Allocation." Proceedings of the 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore Institute of Electrical and Electronics Engineers Inc., 2025. 57-70.

BibTeX: Download