Coalgebraic Nominal Automata with Name Allocation

虽然形式语言理论经典地使用有限字母，但最近人们对无限字母的语言越来越感兴趣，无限字母可用于对无限数据类型（如字符串或自然数）的值进行建模。从这个意义上说，现在有各种各样的数据语言形式化，旨在指定和验证承载或交换数据的结构和进程的属性，例如XML文档、加密协议或动态配置的并行进程。许多这样的形式化都以寄存器为特征，在其中可以存储数据字中遇到的数据值，以便与以后看到的数据值进行比较。在这种意义上，寄存器自动机与最近发展的标称自动机模型是等价的，后者是通过将有限自动机的标准概念从通常意义上的集合转移到具有原子的集合（称为名称）而产生的。在数据语言的形式化中广泛遇到的一个挑战是，中心推理问题，特别是语言包含问题，表现出非基本的计算复杂性，甚至不可判定，除非对计算能力（例如限制在确定性或明确的模型）或寄存器数量施加严格的限制。在我们自己最近的研究中，我们发现在表达能力上有一种相当温和的权衡，可以缓解这个问题。具体来说，我们引入了名称分配自动机模型，其中数据值的新鲜度在标称设置中使用标准的alpha-等价概念建模，即重命名绑定名称。有限词和无限词上的名称分配标称自动机模型允许包含检查相对适度（特别是初级）的复杂性，即使在完全不确定性和无限多寄存器存在的情况下，对表达性也有相当合理的限制（例如，它们可以接受“某些数据值出现两次”的语言，这是确定性或无二义性寄存器自动机所不能接受的）。CoNAN项目的目标是在范围和深度上全面发展名称分配自动机的算法和元理论。具体的研究目标包括名称分配时间逻辑的设计；用于分析命名逻辑和自动机模型的算法和表达的代数和博弈论方法的发展；并将框架扩展到具有额外表达手段的自动机模型，例如名称释放和超越非确定性的分支类型。因此，我们的目标是为广泛的数据语言提供一套全面的方法和算法。

While formal language theory classically works with finite alphabets, there has been increasing recent interest in languages over infinite alphabets, which may be used to model values from infinite data types such as strings or natural numbers. There is, by now, a wide variety of formalisms for data languages in this sense, aimed at specifying and verifying properties of structures and processes that carry or exchange data, such as XML documents, cryptographic protocols, or dynamically configured parallel processes. Many such formalisms feature registers, in which data values encountered in a data word can be stored for comparison with data values seen later. Register automata in this sense have turned out to be equivalent to more recently developed nominal automata models, which arise by transferring the standard concept of finite automata from sets in the usual sense to sets with atoms (referred to as names). A challenge widely encountered in formalisms for data languages is that central reasoning problems, notably the language inclusion problem, exhibit nonelementary computational complexity or even undecidability unless stringent limitations are imposed on either computational power (e.g. restricting to deterministic or unambiguous models) or on the number of registers. In our own recent research, we have identified a fairly mild trade-off in expressiveness that alleviates this problem. Specifically, we have introduced name-allocating automata models, in which freshness of data values is modelled in the nominal setting using the standard notion of alpha-equivalence, i.e. renaming of bound names. Name-allocating nominal automata models on both finite and infinite words allow inclusion checking in comparatively moderate (in particular, elementary) complexity even in presence of full nondeterminism and unboundedly many registers, with fairly reasonable restrictions on expressiveness (e.g. they can accept the language "some data value occurs twice", which is not acceptable by deterministic or unambiguous register automata). The aim of the CoNAN project is a full development of the algorithmics and meta-theory of name-allocating automata in terms of both scope and depth. Specific research goals include the design of name-allocating temporal logics; the development of algebraic and game-theoretic methods for the analysis of the algorithmics and expressiveness of name-allocating logics and automata models; and extension of the framework to automata models featuring additional expressive means such as name deallocation and branching types beyond nondeterminism. We thus aim to provide a comprehensive body of methods and algorithms for a wide range of data languages.