Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. We propose a model checker, named R-CHECK, to allow reasoning about these systems both from an individual- and a system- level. R-CHECK also permits reasoning about interaction protocols and joint missions. R-CHECK supports a high-level input language with symbolic semantics, and provides a modelling convenience for interaction features such as reconfiguration, coalition formation, self-organisation, etc.
翻译:重新配置的多试剂系统由一组自主代理组成,综合互动能力以机会性互动为特点; 代理似乎通过组建集体来重组互动界面,并在互利的基础上进行互动; 寻找设计和分析这些系统行为的方法是一项积极追求的研究目标; 我们提议了一个名为R-CHECCK的示范核对器,以便从个人和系统一级对这些系统进行推理; R-CHECK还允许就互动协议和联合任务进行推理; R-CHECCK支持一种带有象征性语义的高级投入语言,并为诸如重组、联盟形成、自我组织等互动特征提供建模便利。