Graded Monads in the Semantics of Nominal Automata

TL;DR

This paper develops a graded algebraic framework for nominal automata, specifically RNNAs, providing algebraic tools and behavioral equivalence games that unify semantics and improve understanding of data languages.

Contribution

It extends graded monads and algebraic theories to the nominal setting, introducing a behavioral equivalence game for RNNAs and nominal transition systems.

Findings

Algebraic theory capturing local freshness semantics of RNNAs

Development of a graded behavioral equivalence game for nominal automata

Unified algebraic treatment of behavioral equivalences in nominal automata

Abstract

Nominal automata models serve as a formalism for data languages, and in fact often relate closely to classical register models. The paradigm of name allocation in nominal automata helps alleviate the pervasive computational hardness of register models in a tradeoff between expressiveness and computational tractability. For instance, regular nondeterministic nominal automata (RNNAs) correspond, under their local freshness semantics, to a form of lossy register automata. Unlike the full register automaton model, RNNAs allow for inclusion checking in elementary complexity. The semantic framework of graded monads provides a unified algebraic treatment of spectra of behavioural equivalences in the setting of universal coalgebra. In the present work, we extend the associated notion of graded algebraic theory to the nominal setting, and develop a nominal version of the notion of graded behavioural equivalence game. In the arising framework of graded nominal algebra, we conduct an extended case study, giving an algebraic theory capturing the local freshness semantics of RNNAs and the related nominal transition systems. Moreover, we instantiate the general behavioural equivalence game to this setting.