信息不对称下反应式博弈中的机会主义综合

反应式综合是一类在动态且不可控环境中，根据时序逻辑规范构建可证明正确的控制系统（被称为机器人）的方法。这是通过将机器人与其环境之间的交互建模为双人零和博弈来实现的。然而，现有的反应式综合方法假设双方都拥有完全信息，这在许多策略性交互中并不成立。在本文中，我们使用超博弈的一种变体来对机器人与其环境之间的交互进行建模；其中环境对机器人的规范具有不完全信息。该模型使我们能够识别出博弈状态的一个子集，在这些状态下，机器人可以利用不对称信息获得更好的结果，而如果双方拥有对称且完全的信息，这是不可能的。然后，我们通过在时序逻辑规范下使用超博弈定义马尔可夫决策过程（MDP），引入了一种新颖的机会主义综合方法。我们证明，当环境在其感知的必胜区和必败区中采取某种随机策略时，通过遵循机会主义策略，只要机会出现，机器人的博弈结果（以子规范的满足度来衡量）必定只会得到改善。我们通过在存在对手的情况下的机器人运动规划示例，展示了该方法的正确性与最优性。