余代数语言等价的可靠且完备公理化

余代数为研究包括多种自动机在内的动力系统提供了统一框架。在本文中，我们利用系统的余代数视角，以统一的方式研究在何种条件下，相对于行为等价可靠的且完备的演算可以推广到更粗的余代数语言等价，该等价源于将余代数确定化的广义幂集构造。我们证明，通过证明演算表达式模公理构成给定类型函子的有理不动点，可以确立可靠性和完备性。我们的主要结果是，函子 $FT$（其中 $T$ 是描述系统分支（例如非确定性、权重、概率等）的单子）的有理不动点，以“确定化”类型函子 $\bar F$（$F$ 到 $T$-代数范畴的提升）的有理不动点为其商。我们将该框架应用于加权自动机的具体实例，并为其提出了一种新的关于加权语言等价的可靠且完备的演算。作为特例，我们考虑非确定性自动机，并恢复了 Rabinovich 关于语言等价的可靠且完备的演算。