arXiv:2502.13621v1 类型: cross 摘要：在随机动态下的多智能体规划通常使用非中心化的部分可观测量马尔可夫决策过程（MDP）进行形式化，并使用可达性或期望回报规范。在本文中，我们提出了一种不同的方法：我们使用一个描述单个智能体在环境中的操作的MDP，并使用概率超性质来捕捉一组在环境中运作的非中心化智能体的期望时间目标。我们扩展了现有的概率超性质模型检测方法，以处理关联不同智能体路径的时间公式，因此需要多个MDP之间的自组合。通过几个案例研究，我们证明了我们的方法提供了一个灵活且富有表现力的框架，可以增强现有的规划技术的规范能力。此外，我们建立了概率超性质的一个子类与特定类型Dec-MDP规划之间的一个紧密联系，这两种情况我们均证明了不可判定性。这为使用现有的分散规划工具进行概率超性质验证奠定了基础。