Nominal Büchi Automata with Name Allocation

Urbat H, Hausmann D, Milius S, Schröder L (2021)

Publication Type: Conference contribution

Publication year: 2021

Journal

LIPIcs : Leibniz International Proceedings in Informatics Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik

Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

Book Volume: 203

Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs

Event location: Virtual, Online

ISBN: 9783959772037

DOI: 10.4230/LIPIcs.CONCUR.2021.4

Abstract

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.

Authors with CRIS profile

Henning Urbat Lehrstuhl für Informatik 8 (Theoretische Informatik) Stefan Milius Lehrstuhl für Informatik 8 (Theoretische Informatik) Lutz Schröder Lehrstuhl für Informatik 8 (Theoretische Informatik)

Involved external institutions

University of Gothenburg / Göteborgs universitet SE Sweden (SE)

How to cite

APA:

Urbat, H., Hausmann, D., Milius, S., & Schröder, L. (2021). Nominal Büchi Automata with Name Allocation. In Serge Haddad, Daniele Varacca (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Virtual, Online: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.

MLA:

Urbat, Henning, et al. "Nominal Büchi Automata with Name Allocation." Proceedings of the 32nd International Conference on Concurrency Theory, CONCUR 2021, Virtual, Online Ed. Serge Haddad, Daniele Varacca, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2021.

BibTeX: Download