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.

翻译：名义自动机模型作为数据语言的形式化工具，实际上常与经典寄存器模型密切相关。名义自动机中的名称分配范式通过表达能力与计算可处理性之间的权衡，有助于缓解寄存器模型普遍存在的计算困难。例如，在局部新鲜性语义下，正则非确定性名义自动机（RNNA）对应于一种有损寄存器自动机。与完整的寄存器自动机模型不同，RNNA允许在基本复杂度内进行包含性检查。分级单子的语义框架为通用余代数背景下行为等价谱提供了统一的代数处理。在当前工作中，我们将相关的分级代数理论扩展到名义设置，并发展了分级行为等价博弈的名义版本。在由此产生的分级名义代数框架中，我们进行了扩展案例研究，提出了一个代数理论来捕捉RNNA的局部新鲜性语义及相关名义转移系统。此外，我们将通用行为等价博弈实例化到这一设置中。