Alternating Nominal Automata with Name Allocation
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866918024753184768 |
|---|---|
| author | Frank, Florian Hausmann, Daniel Milius, Stefan Schröder, Lutz Urbat, Henning |
| author_facet | Frank, Florian Hausmann, Daniel Milius, Stefan Schröder, Lutz Urbat, Henning |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_03658 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Alternating Nominal Automata with Name Allocation Frank, Florian Hausmann, Daniel Milius, Stefan Schröder, Lutz Urbat, Henning Formal Languages and Automata Theory 68Q45 F.4.3 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. |
| title | Alternating Nominal Automata with Name Allocation |
| topic | Formal Languages and Automata Theory 68Q45 F.4.3 |
| url | https://arxiv.org/abs/2408.03658 |