Multi-agent planning under stochastic dynamics is usually formalised using decentralized (partially observable) Markov decision processes ( MDPs) and reachability or expected reward specifications. In this paper, we propose a different approach: we use an MDP describing how a single agent operates in an environment and probabilistic hyperproperties to capture desired temporal objectives for a set of decentralized agents operating in the environment. We extend existing approaches for model checking probabilistic hyperproperties to handle temporal formulae relating paths of different agents, thus requiring the self-composition between multiple MDPs. Using several case studies, we demonstrate that our approach provides a flexible and expressive framework to broaden the specification capabilities with respect to existing planning techniques. Additionally, we establish a close connection between a subclass of probabilistic hyperproperties and planning for a particular type of Dec-MDPs, for both of which we show undecidability. This lays the ground for the use of existing decentralized planning tools in the field of probabilistic hyperproperty verification.

本研究针对多智能体在随机动力学下的规划问题，提出了一种新方法，利用单一智能体的MDP和概率超属性来捕捉去中心化智能体的时间目标。通过案例研究，我们的方法提供了一种灵活且表达力强的框架，拓宽了现有规划技术的规范能力，并展示了其与某类Dec-MDPs规划的密切联系。

使用概率超属性的去中心化规划