针对串通对手的 opacity-enforcing 获胜策略的合成
Synthesis of Opacity-Enforcing Winning Strategies Against Colluded Opponent
AI总结：
本文研究双人零和博弈中针对串通对手的不透明性执行问题，通过将问题归约为带有观察者信念状态的可达性博弈，合成了P1既能达成秘密时序目标又能保持不透明的获胜策略，并证明了策略不存在时获胜必然以泄露秘密为代价。
摘要：
本文研究图上双人零和博弈中基于语言的 opacity enforcement。在此博弈中，无论对手 player 2 (P2) 选择何种策略，只要 player 1 (P1) 能达成由 finite automaton 语言描述的秘密时序目标，P1 即获胜。此外，P1 旨在获胜的同时，使其目标对信息不完美的被动观察者保持 opaque。然而，P2 与观察者串通，当 P2 无法阻止 P1 达成目标时便揭示 P1 的秘密，因此必须针对 P2 实施 opacity enforcement。我们证明，通过将该问题归约为求解一个 augmented with observer's belief states 的 reachability game，可以计算出 P1 的获胜且 opacity-enforcing 的策略。此外，若此类策略不存在，P1 的获胜必然以向观察者揭示其秘密为代价。我们通过一个小型示例和机器人运动规划问题展示了这一 opacity-enforcement control 的博弈论解决方案。
英文摘要：
This paper studies a language-based opacity enforcement in a two-player, zero-sum game on a graph. In this game, player 1 (P1) wins if it can achieve a secret temporal goal described by the language of a finite automaton, no matter what strategy the opponent player 2 (P2) selects. In addition, P1 aims to win while making its goal opaque to a passive observer with imperfect information. However, P2 colludes with the observer to reveal P1's secret whenever P2 cannot prevent P1 from achieving its goal, and therefore, opacity must be enforced against P2. We show that a winning and opacity-enforcing strategy for P1 can be computed by reducing the problem to solving a reachability game augmented with observer's belief states. Furthermore, if such a strategy does not exist, winning for P1 must entail the price of revealing his secret to the observer. We demonstrate our game-theoretic solution of opacity-enforcement control through a small illustrative example and in a robot motion planning problem.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
