Supported Sets -- A New Foundation For Nominal Sets And Automata

带名称分配的交替名义自动机

Alternating Nominal Automata with Name Allocation

针对无限字母表自动机推理难的问题，提出带名称分配的正则交替名义自动机，证明其寄存器无界时非空与包含问题仍为初等复杂度，可近乎完全去交替，并将Bar-μTL某分支模型检测复杂度提升一个指数级。

On Learning Nominal Automata with Binders

We investigate a learning algorithm in the context of nominal automata, an extension of classical automata to alphabets featuring names. This class of automata captures nominal regular languages; analogously to the classical language theory, nominal automata have been shown to characterise nominal regular expressions with binders. These formalisms are amenable to abstract modelling resource-aware computations. We propose a learning algorithm on nominal regular languages with binders. Our algorithm generalises Angluin's L* algorithm with respect to nominal regular languages with binders. We sho…

带名称分配的 nominal 树自动机

Nominal Tree Automata With Name Allocation

针对数据树自动机语言包含判定难的问题，提出基于nominal集合与显式名称分配的树自动机模型，支持非确定性与任意寄存器数，且语言包含检查为参数化指数时间的初等复杂度。

Automata theory in nominal sets

We study languages over infinite alphabets equipped with some structure that can be tested by recognizing automata. We develop a framework for studying such alphabets and the ensuing automata theory, where the key role is played by an automorphism group of the alphabet. In the process, we generalize nominal sets due to Gabbay and Pitts.

Nominal Cellular Automata

The emerging field of Nominal Computation Theory is concerned with the theory of Nominal Sets and its applications to Computer Science. We investigate here the impact of nominal sets on the definition of Cellular Automata and on their computational capabilities, with a special focus on the emergent behavioural properties of this new model and their significance in the context of computation-oriented interpretations of physical phenomena. A preliminary investigation of the relations between Nominal Cellular Automata and Wolfram's Elementary Cellular Automata is also carried out.

Separation and Renaming in Nominal Sets

Nominal sets provide a foundation for reasoning about names. They are used primarily in syntax with binders, but also, e.g., to model automata over infinite alphabets. In this paper, nominal sets are related to nominal renaming sets, which involve arbitrary substitutions rather than permutations, through a categorical adjunction. In particular, the left adjoint relates the separated product of nominal sets to the Cartesian product of nominal renaming sets. Based on these results, we define the new notion of separated nominal automata. These automata can be exponentially smaller than classical …

带提示自动机与名义自动机的查询学习

Query Learning of Advice and Nominal Automata

本研究采用Chase和Freitag提出的基于组合复杂度度量的查询学习界证明方法，推导了带提示DFA的首个查询复杂度上界，并对名义DFA的相关结果做出了性质上的改进。

Nominal Automata with Name Binding

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 …

A Linear-Time Nominal $μ$-Calculus with Name Allocation

Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, serve the verification of processes or documents with data. They relate tightly to formalisms over nominal sets, such as nondetermininistic orbit-finite automata (NOFAs), where names play the role of data. Reasoning problems in such formalisms tend to be computationally hard. Name-binding nominal automata models such as regular nondeterministic nominal automata (RNNAs) have been shown to be computationally more tractable. In the present paper, we introduce a linear-time fixpoint logic Ba…

A decidable class of (nominal) omega-regular languages over an infinite alphabet

We define a class of languages of infinite words over infinite alphabets, and the corresponding automata. The automata used for recognition are a generalisation of deterministic Muller automata to the setting of nominal sets. Remarkably, the obtained languages are determined by their ultimately periodic fragments, as in the classical case. Closure under complement, union and intersection, and decidability of emptiness and equivalence are preserved by the generalisation. This is shown by using finite representations of the (otherwise infinite-state) defined class of automata.

拓扑斯中的自动机，以及一般的Myhill-Nerode定理

Automata in toposes, and general Myhill-Nerode theorems

本文将函子自动机方法扩展至任意具有自然数对象的初等拓扑斯并建立一般Myhill-Nerode定理，作为特例恢复了关于轨道有限nominal automata的已知结果。

Automata Learning: An Algebraic Approach

We propose a generic categorical framework for learning unknown formal languages of various types (e.g. finite or infinite words, weighted and nominal languages). Our approach is parametric in a monad T that represents the given type of languages and their recognizing algebraic structures. Using the concept of anautomata presentation of T-algebras, we demonstrate that the task of learning a T-recognizable language can be reduced to learning an abstract form of algebraic automaton whose transitions are modeled by a functor. For the important case of adjoint automata, we devise a learning algori…

有限支持结构中的有限上下文语义

Finite-Context Semantics in Finitely Supported Structures

本文在有限支持结构中提出有限上下文语义，证明单调有限支持变换器在完备格中具有不动点，并给出布尔谓词的有限收敛界，应用于自动机、模态语义、抽象解释和资源重写等领域。

使用自定义控制脉冲在IBMQ中实现量子有限自动机

Implementing a Quantum Finite Automaton in IBMQ using Custom Control Pulses

本研究针对量子有限自动机在实际器件中因退相干影响长字符串计算的问题，采用脉冲级编程校准专用快速单量子比特门，在IBM-Q环境下显著降低计算误差、缩短延迟，提升了自动机支持的最大计算长度。