Graded Monads in the Semantics of Nominal Automata
Hannes Schulze, Lutz Schröder, Üsame Cengiz
TL;DR
The paper advances the semantics of data languages by marrying nominal automata with graded semantics. It extends graded monad theory to nominal sets through graded nominal algebra, producing depth-1 graded monads that capture local freshness semantics for regular nondeterministic nominal automata (RNNAs) and their bar-language representations. A detailed case study for global and local freshness demonstrates soundness and completeness of the algebraic framework and shows that both semantics can be modeled by depth-1 graded monads, enabling precise language and trace characterizations. The work provides algebraic tools for reasoning about nominal automata, with potential for modal-logical characterizations and broader nominal settings.
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, and unlike the full register automaton model 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. In the arising framework of graded nominal algebra, we give an algebraic theory capturing the local freshness semantics of RNNAs.