面向随机多智能体系统能力的假设-保证验证

对战略能力进行模型检验是一个极其困难的问题，尤其是在智能体拥有不完美信息且处于随机环境中时更为如此。假设-保证推理在这里大有裨益，提供将复杂问题分解为少数更易子问题的方式。在本文中，我们提出了几种用于带不完美信息的概率交替时间逻辑假设-保证验证方案。我们证明了这些方案的完备性，并讨论了其完备性。在此过程中，我们还提出了一种新的非概率交替时间逻辑变体，其中战略模态捕获“最多实现 $\varphi$”的含义，类似于 Levesque 的“仅知道”逻辑。