重访定时自动机网络的局部时间语义

我们研究了一种基于区域的定时自动机可达性问题方法。挑战在于缓解考虑并行工作的定时自动机网络时搜索空间的大小爆炸。在定时设定下，这种爆炸尤为明显，因为即便进程局部动作的不同交错也可能导致不同区域。Salah 等人于 2006 年已证明所有这些不同区域的并集也是一个区域。该观察被用于一种算法，该算法不时检测并将这些区域聚合成单一区域。我们表明，利用 Bengtsson 等人于 1998 年提出的局部时间语义及相关的局部区域概念，可更高效地计算此类聚合区域。接着，我们指出已有方法中确保局部区域图计算终止的一处缺陷。我们借助一种新算法修复该问题，该算法构建局部区域图并使用基于（标准）区域的抽象技术以保证终止。我们在标准实例上评估了我们的算法。在多个实例中，我们观察到搜索空间降低了一个数量级。在其余实例上，该算法表现如同标准区域算法。