半环上加权自动机互模拟的余代数刻画

加权自动机是非确定性自动机的一种推广，它将从半环 $K$ 中取出的权重与每个转移和每个状态相关联。其行为可形式化为加权语言等价或加权互模拟。本文在以下两类余代数框架中探讨加权自动机的性质：(i) 半环 $K$ 上半模及 $K$-线性映射的范畴 $\mathsf{SMod}$，以及 (ii) 集合与映射的范畴 $\mathsf{Set}$。我们证明，这两种情况下相应最终余代数所定义的行为等价分别刻画了加权语言等价与加权互模拟。这些结果推广了 Bonchi 等人早期使用向量空间与线性映射范畴 $\mathsf{Vect}$ 作为权重取自域 $K$ 的加权自动机底层模型的工作。我们工作的关键步骤是利用泛代数意义下 $K$-线性映射的核概念，将 Boreale 的线性关系和线性互模拟概念从向量空间推广到半模。我们还给出了一个用于计算加权语言等价的前向划分精化抽象过程。由于定义在半环上的加权自动机问题一般是不可判定的，该过程仅在特定情况下保证终止。我们给出了过程终止的充分条件。尽管结果与 Bonchi 等人相似，我们的许多证明是新的，特别是关于刻画加权语言等价的 $\mathsf{SMod}$ 中余代数的那些证明。