Nominal B\"uchi Automata with Name Allocation

TL;DR

This paper introduces a new automata model called B"uchi RNNAs for infinite words over infinite alphabets with name binding, proving that language inclusion is decidable, which benefits model checking applications.

Contribution

The paper presents B"uchi RNNAs, a novel automata model for infinite bar strings with binding, and establishes the decidability of language inclusion for this model.

Findings

Decidable and elementary language inclusion problem for B"uchi RNNAs.

Automata model effectively handles name binding and resource allocation.

Suitable for applications in model checking over infinite alphabets.

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 omega-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\"uchi automata (B\"uchi 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\"uchi-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\"uchi RNNAs is decidable and in fact elementary. This makes B\"uchi RNNAs a suitable tool for applications in model checking.