Model checking multi-agent systems with MABLE
Model checking multi-agent systems with MABLE
复制标题
使用 MABLE 检查多智能体系统模型
DOI：
10.1145/544862.544965
复制
发表时间：
2002
影响因子：
7.5
通讯作者：
S. Parsons
中科院分区：
文献类型：
--
作者：
M. Wooldridge;Michael Fisher;M. Huget;S. Parsons
MABLE是一种用于设计和自动验证多代理系统的语言。MABLE本质上是一种传统的命令式编程语言，通过面向代理的编程范式的构造来丰富。一个MABLE系统包含许多代理，使用MABLE命令式编程语言编程。MABLE中的主体具有由信念、欲望和意图组成的精神状态。代理使用请求和通知执行语进行通信，采用fipa代理通信语言的风格。MABLE系统可以通过增加关于系统的正式声明来增强，使用量化的线性时间信念-愿望-意图逻辑来表达。MABLE已经完全实现，并利用自旋模型检查器自动验证声明的真实性或虚假性。
MABLE is a language for the design and automatic verification of multi-agent systems. MABLE is essentially a conventional imperative programming language, enriched by constructs from the agent-oriented programming paradigm. A MABLE system contains a number of agents, programmed using the MABLE imperative programming language. Agents in MABLE have a mental state consisting of beliefs, desires and intentions. Agents communicate using request and inform performatives, in the style of the fipa agent communication language. MABLE systems may be augmented by the addition of formal claims about the system, expressed using a quantified, linear temporal belief-desire-intention logic. MABLE has been fully implemented, and makes use of the spin model checker to automatically verify the truth or falsity of claims.