Abstraction in model checking multi-agent systems
Abstraction in model checking multi-agent systems
复制标题
DOI：
10.1145/1558109.1558144
复制
发表时间：
2009-05
期刊：
影响因子：
--
通讯作者：
F. Russo
中科院分区：
文献类型：
--
作者：
F. Russo
我们提出了一种保持时间-认知规范的多智能体系统的抽象技术。我们抽象出一个定义在解释系统框架中的多智能体系统，它通过折叠系统中每个智能体的局部状态和动作来实现。我们证明了所得到的抽象系统模拟了具体系统，由此我们得到了一个保持定理：如果一个时间-认知规范在抽象系统上成立，该规范也在具体系统上成立。原则上，这允许我们对抽象系统而不是具体系统进行模型检查，从而节省了验证步骤中的时间和空间。我们用两个例子来说明抽象技术。第一个示例是纸牌游戏，它说明了在典型的MAS场景中进行模型检查可能会节省的成本。在第二个例子中，抽象技术用于验证具有任意大的数据域的通信协议。
We present an abstraction technique for multi-agent systems preserving temporal-epistemic specifications. We abstract a multi-agent system, defined in the interpreted systems framework, by collapsing the local states and actions of each agent in the system. We show that the resulting abstract system simulates the concrete system, from which we obtain a preservation theorem: If a temporal-epistemic specification holds on the abstract system, the specification also holds on the concrete one. In principle this permits us to model check the abstract system rather than the concrete one, thereby saving time and space in the verification step. We illustrate the abstraction technique with two examples. The first example, a card game, illustrates the potential savings in the cost of model checking a typical MAS scenario. In the second example, the abstraction technique is used to verify a communication protocol with an arbitrarily large data domain.