用概率超性质建模多智能体规划，更灵活地表达协同目标。
Decentralized Planning Using Probabilistic Hyperproperties
- 以单智能体MDP为基础，通过路径间关系描述多智能体协作目标。
- 扩展模型检验技术，支持跨智能体路径的时序逻辑验证。
- 为多智能体规划与超性质验证提供了理论桥梁，适合系统验证研究者。
在随机动态环境下进行多智能体规划通常采用去中心化（部分可观测）马尔可夫决策过程（Dec-MDPs）及可达性或期望奖励规范。本文提出新方法：使用一个描述单个智能体行为的MDP，并借助概率超性质来捕捉一组去中心化智能体在环境中运行时的时序目标。我们扩展了现有概率超性质模型检验技术，以处理涉及不同智能体路径的时序公式，从而需要对多个MDP进行自组合。通过若干案例研究，我们证明该方法在规范表达能力上优于现有规划技术。此外，我们揭示了一类概率超性质与特定类型Dec-MDP规划之间的紧密联系，并证明两者均不可判定，为利用现有的去中心化规划工具推进概率超性质验证奠定了基础。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。