面向不完全信息多智能体系统策略性质验证的研究
多智能体系统
2023-06-19 v1 计算机科学中的逻辑
摘要
在策略推理的逻辑中，主要挑战在于其在不完全信息与完美回忆语境下的验证。本工作展示一种近似验证不完全信息与完美回忆下交替时间时序逻辑（ATL*）的技术，该问题已知不可判定。给定模型 M 与公式 ，我们提出一种验证过程，生成 M 的子模型，其中每个子模型 M' 满足 的子公式 且在 M' 中 的验证可判定。随后，我们使用 CTL* 模型检测给出 在 M 上的验证结果。我们证明该过程的复杂度类与完美信息与完美回忆下 ATL* 模型检测相同，给出了实现该过程的工具并提供了实验结果。
引用
@article{arxiv.2112.13621,
title = {Towards the Verification of Strategic Properties in Multi-Agent Systems with Imperfect Information},
author = {Angelo Ferrando and Vadim Malvone},
journal= {arXiv preprint arXiv:2112.13621},
year = {2023}
}