2026-07-26T00:36:21Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:14381 2024-03-06T10:54:16Z ddc:004 open_access

Nominal Büchi Automata with Name Allocation Urbat, Henning Hausmann, Daniel Milius, Stefan Schröder, Lutz Data languages infinite words nominal sets inclusion checking Infinite words over infinite alphabets serve as models of the temporal development of the allocation and (re-)use of resources over linear time. We approach ω-languages over infinite alphabets in the setting of nominal sets, and study languages of infinite bar strings, i.e. infinite sequences of names that feature binding of fresh names; binding corresponds roughly to reading letters from input words in automata models with registers. We introduce regular nominal nondeterministic Büchi automata (Büchi RNNAs), an automata model for languages of infinite bar strings, repurposing the previously introduced RNNAs over finite bar strings. Our machines feature explicit binding (i.e. resource-allocating) transitions and process their input via a Büchi-type acceptance condition. They emerge from the abstract perspective on name binding given by the theory of nominal sets. As our main result we prove that, in contrast to most other nondeterministic automata models over infinite alphabets, language inclusion of Büchi RNNAs is decidable and in fact elementary. This makes Büchi RNNAs a suitable tool for applications in model checking. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Henning Urbat and Daniel Hausmann and Stefan Milius and Lutz Schröder 2021 Is Part Of LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2021.4 urn:nbn:de:0030-drops-143813 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.4 eng https://creativecommons.org/licenses/by/4.0/legalcode