条件简单时序网络动态一致性检查中的瞬时反应时间——扩展版及改进的上界

CSTN 是一种基于约束的图形式化方法，用于条件时序规划。为解决 DC-检查问题，我们在 [Comin and Rizzi, TIME 2015] 中引入了 epsilon-DC（一种更精细、更现实的 DC 概念），并给出了算法解。epsilon-DC 概念本身即有意义，而 [Comin and Rizzi, TIME 2015] 中的 epsilon-DC-检查算法基于反应时间满足 epsilon > 0 的假设，遗留了 epsilon = 0 时的问题。本文引入并研究 pi-DC，一种具有瞬时反应时间（即规划器可在观测发生的同一瞬间对任何观测做出反应）的合理 DC 概念。首先，我们通过反例证明 pi-DC 不等价于 0-DC，且 0-DC 实际上不适合对具有瞬时反应时间的 DC 建模。这表明我们先前工作中得到的主要结果在其原有形式下不能直接应用于 epsilon=0 的情形。受此启发，作为第二项贡献，我们扩展了先前的工具以处理 pi-DC，引入了 ps-树的概念，并指出了 pi-DC 与 HyTN-一致性之间的关系。第三，我们识别出从 pi-DC-检查到 DC-检查的一个简单归约。这使我们能够设计并分析第一个可靠且完备的 pi-DC-检查过程。值得注意的是，所提算法的时间复杂度在命题字母数量上仍保持（伪）单指数级。最后，我们观察到该技术可用于实际从 pi-DC 归约到 1-DC，从而进一步改进 pi-DC-检查时间复杂度中的指数。