Nominal automata with name binding
From MaRDI portal
Abstract: Automata models for data languages (i.e. languages over infinite alphabets) often feature either global or local freshness operators. We show that Bollig et al.'s session automata, which focus on global freshness, are equivalent to regular nondeterministic nominal automata (RNNA), a natural nominal automaton model with explicit name binding that has appeared implicitly in the semantics of nominal Kleene algebra (NKA), an extension of Kleene algebra with name binding. The expected Kleene theorem for NKA is known to fail in one direction, i.e. there are nominal languages that can be accepted by an RNNA but are not definable in NKA; via session automata, we obtain a full Kleene theorem for RNNAs for an expression language that extends NKA with unscoped name binding. Based on the equivalence with RNNAs, we then slightly rephrase the known equivalence checking algorithm for session automata. Reinterpreting the data language semantics of name binding by unrestricted instead of clean alpha-equivalence, we obtain a local freshness semantics as a quotient of the global freshness semantics. Under local freshness semantics, RNNAs turn out to be equivalent to a natural subclass of Bojanczyk et al.'s nondeterministic orbit-finite automata. We establish decidability of inclusion under local freshness by modifying the RNNA-based algorithm; in summary, we obtain a formalism for local freshness in data languages that is reasonably expressive and has a decidable inclusion problem.
Recommendations
Cites work
- A fully abstract denotational semantics for the \(\pi\)-calculus
- A robust class of data languages and an application to learning
- Automata and Logics for Words and Trees over an Infinite Alphabet
- Automata theory in nominal sets
- Completeness and incompleteness in nominal Kleene algebra
- Completeness results for parameterized space classes
- Finite state machines for strings over infinite alphabets
- Finite-memory automata
- Finite-memory automata with non-deterministic reassignment
- Foundations of nominal techniques: logic and semantics of variables in abstract syntax
- Fresh-register automata
- Freshness and Name-Restriction in Sets of Traces with Names
- History-register automata
- scientific article; zbMATH DE number 2086669 (Why is no real title available?)
- scientific article; zbMATH DE number 5254145 (Why is no real title available?)
- Imperative programming in sets with atoms
- Leaving the nest: nominal techniques for variables with interleaving scopes
- LTL with the freeze quantifier and register automata
- Nominal Domain Theory for Concurrency
- Nominal Kleene coalgebra
- Nominal sets. Names and symmetry in computer science
- On nominal regular languages with binders
- Regular expressions for data words
- Regular expressions for languages over infinite alphabets
- Unambiguity in automata theory
- Universal coalgebra: A theory of systems
- Variable automata over infinite alphabets
- Walking on data words
Cited in
(13)- From generic partition refinement to weighted tree automata minimization
- Coalgebraic semantics for nominal automata
- Automata theory in nominal sets
- On nominal regular languages with binders
- Residuality and learning for nondeterministic nominal automata
- scientific article; zbMATH DE number 7559500 (Why is no real title available?)
- A Kleene theorem for nominal automata
- A coalgebraic view on reachability
- Regular and context-free nominal traces
- Towards nominal context-free model-checking
- Fresh-register automata
- Generic partition refinement and weighted tree automata
- Nominal tree automata with name allocation
This page was built for publication: Nominal automata with name binding
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2988364)
