论文部分内容阅读
n-精化关系在计算机科学领域中发挥着重要作用。在理论计算机科学中，学者们常用互模拟来刻画状态转换系统（例如，实时控制系统）之间的行为关系，当两个系统之间存在互模拟等价关系时，从某种意义上来说，一个系统的行为可以模拟另一个系统，反之亦然。但是互模拟关系并不能使得在模型检测时所需检测状态空间得到明显的缩减，因此引入了精化关系。精化与互模拟的区别在于，其对向前条件没有限制，如果精化关系满足向前条件，那么该精化关系也是互模拟关系。在刻画系统状态之间精化关系是否在有限的可达关系上成立这个问题时，需要将精化扩展到n-