Synthesis of Opacity-Enforcing Winning Strategies Against Colluded Opponent
Synthesis of Opacity-Enforcing Winning Strategies Against Colluded Opponent
复制标题
DOI：
10.1109/cdc49753.2023.10384109
复制
发表时间：
2023-04
期刊：
影响因子：
--
通讯作者：
Chongyang Shi;A. Kulkarni;Hazhar Rahmani;Jie Fu
中科院分区：
文献类型：
--
作者：
Chongyang Shi;A. Kulkarni;Hazhar Rahmani;Jie Fu
本文研究了图上两人零和博弈中基于语言的不透明度执行问题。在这场博弈中，无论对手玩家2(P2)选择什么策略，只要他能实现用有限自动机的语言描述的秘密时间目标，那么玩家1(P1)就赢了。此外，P1的目标是获胜，同时使其目标对具有不完全信息的被动观察者不透明。然而，当P2不能阻止P1实现其目标时，P2与观察者串通，揭示了P1‘S秘密，因此，必须对P2强制不透明。我们证明了通过将问题归结为求解增加了观测者信念状态的可达性博弈，可以计算出P1的制胜和不透明强制策略。此外，如果不存在这样的策略，赢得P1必须付出向观察者透露他的秘密的代价。我们通过一个小的说明性例子和一个机器人运动规划问题来演示我们的不透明强制控制的博弈论解决方案。
This paper studies language-based opacity enforcement in a two-player, zero-sum game on a graph. In this game, player 1 (P1) wins if he 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 the 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.