弱双相似性不可判定性：并发系统验证的新边界

弱双相似性问题在理论计算机科学领域是一个核心研究主题，特别是在行为等价性的探索中占据重要地位。它探讨了两个系统在执行过程中是否具有类似的行为特征，其中弱双相似性是相对较弱的一种等价性标准，相比于强互模拟，它允许更多的差异。这种等价性对于一些基础模型如下推过程（PDA）、过程代数（PA）以及多集自动机（MSA，也称为并行下推过程，PPDA）来说是不可判定的，这意味着没有有效的算法能够确定两个这样的系统是否真的在弱双相似意义上相等。 尽管在基本进程代数（BPA）和基本并行进程（BPP）的上下文中，弱双相似性的可判定性是一个未解决的问题，但本研究进一步揭示了这一不可判定性质的普遍性。作者证明了即使在BPA和BPP的赋范子类扩展有限约束系统中，弱互模拟等价问题依然是不可判定的。这暗示了在这些高级模型中，寻找弱等价性的决定性方法仍然遥不可及。 研究还指出，由于现代软件系统的复杂性和数据类型的无限性，自动化验证往往需要将它们简化为有限状态系统进行处理。不同的规格化形式主义，如Petri网（PN）、下推进程（PDA）和过程代数（如BPA、BPP或PA），各有其适用场景和局限性。在这个背景下，Mayr引入的过程重写系统（PRS）作为一种处理无限状态系统的工具，它通过重写规则来描述系统的动态行为。 总结来说，这篇论文深入探讨了弱双相似性和弱互模拟在并发系统验证中的重要性，揭示了其不可判定性质，并且强调了在处理复杂系统时如何适当地选择和运用不同的理论框架。这项工作不仅对理论研究有深远影响，也为实际的系统设计和验证提供了新的理解与挑战。