确定性自上而下树自动机的等价检查问题

我们提出了一种高效算法，用于检查自上而下确定性有限树自动机（DFTAs）中状态的语言等价性。与字符串自动机不同，树自动机 operate over 层次结构，这给算法分析带来了独特挑战。我们的做法将等价检查问题归约为检查语言论方程组的可解性问题，这些方程指定了 DFTA 的行为。通过构建此类方程组并通过置换和冲突检测规则进行系统化操作，我们开发了一种决策程序，用于确定两个状态是否接受相同的树语言。我们形式地证明了算法的正确性和终止性，并在增强了带指针的随机访问机（RAM）计算模型下，建立了其最坏情况时间复杂度为 $O(n^2)$。