代数 Petri 网的齐次方程

代数 Petri 网是一种用于建模分布式系统和算法的形式化方法，通过结合 Petri 网和代数规范来描述控制流和数据流。指定代数 Petri 网模型 $N$ 正确性的一种方法是，基于项替换和阿贝尔群 $G$ 中的系数，在 $N$ 的库所上指定一个线性方程 $E$。那么，$E$ 在 $N$ 中有效当且仅当 $E$ 在 $N$ 的每个可达标识中有效。由于代数 Petri 网的表达能力，其有效性一般是不可判定的。稳定线性方程构成了一类有效性可判定的线性方程。库所不变量给出了所有稳定线性方程的一种理解透彻但不完备的刻画。在本文中，通过将自身限制在 Herbrand 结构上的项解释而不考虑进一步的等式公理，我们提供了齐次线性方程这一子类稳定性的完备刻画。基于此，我们证明了当 $G$ 是循环群时，齐次线性方程的稳定性是可判定的。