加权定时游戏中鲁棒最优策略的合成

加权定时游戏（WTG）是描述涉及实时问题的控制合成问题最常用的模型。合成的策略依赖于对时间流逝的完美测量，这在实际中并不现实。为了产生对时序不确定性具有容错性的策略，我们依赖于最初用于时序自动机的鲁棒性概念。具体而言，WTG是由两个玩家在带有整数权重的时序自动机中进行的零和游戏，其中一个玩家（称为Min）希望到达目标位置并最小化累计权重。本文中，我们将底层时序自动机置于一种取决于某些参数（代表最大可能扰动）的语义下， opponent（对手）此外还能扰动Min所选择的延迟。于是，鲁棒值问题可表述为：给定某个阈值，是否存在正的扰动且存在一种Min的策略，确保无论对手如何操作，都能以累计权重低于阈值的方式到达目标。我们提供了该鲁棒值问题的首个可判决性结果，通过以参数化方式计算鲁棒值函数来实现这一点，针对的是被称为WTG的发散类（该类被引入以在不限制时钟数量的WTG中实现对（经典）值的可判决性）。为此，我们显示鲁棒值是某些算子的不动点，就像在价值迭代算法中所做的那样。随后，我们小心地结合了两种表示方法：用于分析WTG的分段仿射函数引入于[1]，以及用于分析时序自动机鲁棒性的缩小差分界限矩阵（shrunken Difference Bound Matrices）引入于[29]。最后，我们还研究了质性决策问题，解决了一个关于鲁棒可达性的开放问题，表明对于一般WTG，鲁棒可达性是EXPTIME-complete的。