基于SMT的参数化多智能体系统安全性验证
人工智能
2020-08-17 v2 多智能体系统
摘要
本文研究参数化多智能体系统（MASs）的验证，特别是验证给定MAS中由给定状态公式表征的不期望状态是否可达，即该MAS是否不安全。该MAS是参数化的，模型仅描述可能的智能体模板的有限集合，而每个模板的具体智能体实例的实际数量是无限的且无法预见。这使得状态空间是无限的。由于安全性当然可能取决于系统中智能体实例的数量，验证结果必须无论该数量如何都正确。我们通过基于可满足性模理论（SMT）的无限状态模型检测来解决此问题，依赖于基于数组系统的理论：我们将参数化MAS表示为特定的基于数组的系统，在MAS的两种执行语义下，我们称之为并发和交错。我们在这些假设下证明了可判定性结果，并说明了我们的实现方法，称为SAFE：群体安全检测器（Swarm Safety Detector），其基于第三方模型检测器MCMT，我们对其进行了实验评估。最后，我们讨论了此方法如何适用于比文献中现有最先进解决方案更丰富的参数化和数据感知MAS设置，我们将其留作未来工作。
引用
@article{arxiv.2008.04774,
title = {SMT-based Safety Verification of Parameterised Multi-Agent Systems},
author = {Paolo Felli and Alessandro Gianola and Marco Montali},
journal= {arXiv preprint arXiv:2008.04774},
year = {2020}
}