基于平均收益博弈的条件简单时序网络动态一致性：一种单指数时间DC检测

条件简单时序网络（CSTN）是一种用于条件时序规划的基于约束的图形式化方法。它提供了比Tsamardinos、Vidal和Pollack的等价CSTP模型更灵活的形式化，其衍生主要作为一种可靠形式化。CSTN和CSTP出现三种一致性概念：弱、强和动态。动态一致性是最有趣的概念，但也最具挑战性，且曾被猜想难以判定。Tsamardinos、Vidal和Pollack给出了一个双指数时间算法，用于判定CSTN是否动态一致，并在肯定情况下生成指数规模的动态执行策略。在本工作中，我们证明了判定CSTN是否动态一致是coNP难的，并针对该问题给出了首个单指数时间算法，且在输入CSTN动态一致时生成动态执行策略。该算法基于与平均收益博弈（Mean Payoff Games）的新颖联系，后者是一类图上的两人组合博弈，以在模型检测和形式化验证中的应用而闻名。此联系的呈现通过超时序网络（Hyper Temporal Network）模型中介，它是简单时序网络的可处理推广，其一致性检查等价于判定平均收益博弈。为分析算法，我们引入了动态一致性的精细化概念，称为\epsilon-动态一致性，并对反应时间\hat{\varepsilon}的临界值给出了尖锐下界分析，在该值处CSTN从动态一致转变为非动态一致。此\hat{\varepsilon}分析中引入的证明技术更一般地适用于处理包含严格不等式的线性差分约束。