判定时间自动机关系及其博弈刻画的统一方法

本文提出了一种统一方法，用于判定两个时间自动机状态之间的各种互模拟、模拟等价和预序关系。我们提出了一种基于区域（zone）的方法来判定这些关系，该方法消除了经典方法中区域图或区域图的显式乘积构造。我们的方法具有通用性，可用于判定多种时间关系。我们还提出了这些时间关系的博弈刻画，并表明博弈层次反映了时间关系的层次。人们可以获得无限的博弈层次，因此博弈刻画进一步指出了定义尚未研究的新时间关系的可能性。博弈刻画还有助于我们得出一个公式，该公式编码了两个非时间互模拟状态之间的区分。此类区分公式也可生成用于除时间互模拟之外的许多其他关系。