Nominal Automata with Name Deallocation
Simon Prucker, Stefan Milius, Lutz Schr\"oder

TL;DR
This paper introduces a new nominal automaton model for data words with explicit memory allocation and deallocation, extending existing models and establishing a Kleene theorem with determinization capabilities.
Contribution
It presents a novel automaton model that incorporates deallocation, along with a finite NFA representation and a Kleene theorem, advancing the theory of nominal automata.
Findings
Established a Kleene theorem for the new automaton model
Demonstrated that the model allows for determinization
Extended nominal automata to include deallocating transitions
Abstract
Data words with binders formalize concurrently allocated memory. Most name-binding mechanisms in formal languages, such as the -calculus, adhere to properly nested scoping. In contrast, stateful programming languages with explicit memory allocation and deallocation, such as C, commonly interleave the scopes of allocated memory regions. This phenomenon is captured in dedicated formalisms such as dynamic sequences and bracket algebra, which similarly feature explicit allocation and deallocation of letters. One of the classical formalisms for data languages are register automata, which have been shown to be equivalent to automata models over nominal sets. In the present work, we introduce a nominal automaton model for languages of data words with explicit allocation and deallocation that strongly resemble dynamic sequences, extending existing nominal automata models by adding…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · semigroups and automata theory · Logic, programming, and type systems
