半环上加权自动机互模拟的余代数
Coalgebras for Bisimulation of Weighted Automata over Semirings
AI总结：
本文在半模和集合范畴的余代数框架下研究加权自动机，证明最终余代数分别刻画加权语言等价与加权互模拟，并推广了线性关系概念，提出前向划分细化算法及终止条件。
摘要：
加权自动机是非确定性自动机的一种推广，它为每个转移和每个状态关联一个从半环 $K$ 中选取的权重。它们的行为可以形式化为加权语言等价或加权互模拟。在本文中，我们在余代数框架下探讨加权自动机的性质，该框架基于 (i) 半环 $K$ 上的半模与 $K$-线性映射构成的范畴 $\mathsf{SMod}$，以及 (ii) 集合与映射构成的范畴 $\mathsf{Set}$。我们证明了在这两种情况下，由相应的最终余代数所定义的行为等价分别刻画了加权语言等价和加权互模拟。这些结果扩展了 Bonchi 等人早先的工作，他们使用向量空间与线性映射构成的范畴 $\mathsf{Vect}$ 作为底层模型，处理权重取自域 $K$ 的加权自动机。我们工作的关键步骤是利用泛代数意义下 $K$-线性映射的核这一概念，将 Boreale 的线性关系和线性互模拟概念从向量空间推广到半模。我们还提供了一种用于计算加权语言等价的前向划分细化的抽象过程。由于定义在半环上的加权自动机问题通常不可判定，该过程仅在特殊情况下保证终止。我们给出了该过程终止的充分条件。尽管结果与 Bonchi 等人的相似，但我们的许多证明是全新的，尤其是关于 $\mathsf{SMod}$ 中刻画加权语言等价的余代数的那些证明。
英文摘要：
Weighted automata are a generalization of nondeterministic automata that associate a weight drawn from a semiring $K$ with every transition and every state. Their behaviours can be formalized either as weighted language equivalence or weighted bisimulation. In this paper we explore the properties of weighted automata in the framework of coalgebras over (i) the category $\mathsf{SMod}$ of semimodules over a semiring $K$ and $K$-linear maps, and (ii) the category $\mathsf{Set}$ of sets and maps. We show that the behavioural equivalences defined by the corresponding final coalgebras in these two cases characterize weighted language equivalence and weighted bisimulation, respectively. These results extend earlier work by Bonchi et al. using the category $\mathsf{Vect}$ of vector spaces and linear maps as the underlying model for weighted automata with weights drawn from a field $K$. The key step in our work is generalizing the notions of linear relation and linear bisimulation of Boreale from vector spaces to semimodules using the concept of the kernel of a $K$-linear map in the sense of universal algebra. We also provide an abstract procedure for forward partition refinement for computing weighted language equivalence. Since for weighted automata defined over semirings the problem is undecidable in general, it is guaranteed to halt only in special cases. We provide sufficient conditions for the termination of our procedure. Although the results are similar to those of Bonchi et al., many of our proofs are new, especially those about the coalgebra in $\mathsf{SMod}$ characterizing weighted language equivalence.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
