Verification of multi-agent systems with public actions against strategy logic
Verification of multi-agent systems with public actions against strategy logic
复制标题
基于策略逻辑的公共行为的多智能体系统验证
DOI：
10.1016/j.artint.2020.103302
复制
发表时间：
2020-08-01
影响因子：
14.4
通讯作者：
Rubin, Sasha
中科院分区：
文献类型：
--
作者：
Belardinelli, Francesco;Lomuscio, Alessio;Rubin, Sasha
模型检查多代理系统，其中代理是分布式的，因此可能有不同的观察世界，对战略行为是一个复杂的问题，在许多设置。传统上有两种方法来改善这种复杂性：对代理人的观察强加一个层次结构，或者限制代理人的行为，使它们可以被所有代理人观察到。我们研究后一种系统，因为它们更适合于建模理性代理。特别是，我们定义了多智能体系统，其中所有的行动都是公共的，并研究了这种系统的模型检查问题，对战略逻辑与平等，一个非常丰富的战略逻辑，可以表达相关的概念，如纳什均衡，帕累托最优，由于新增加的平等，也进化稳定的战略。主要结果是相应的模型检验问题是可判定的。(C)2020爱思唯尔B.V.保留所有权利。
Model checking multi-agent systems, in which agents are distributed and thus may have different observations of the world, against strategic behaviours is known to be a complex problem in a number of settings. There are traditionally two ways of ameliorating this complexity: imposing a hierarchy on the observations of the agents, or restricting agent actions so that they are observable by all agents. We study systems of the latter kind, since they are more suitable for modelling rational agents. In particular, we define multi-agent systems in which all actions are public and study the model checking problem of such systems against Strategy Logic with equality, a very rich strategic logic that can express relevant concepts such as Nash equilibria, Pareto optimality, and due to the novel addition of equality, also evolutionary stable strategies. The main result is that the corresponding model checking problem is decidable. (C) 2020 Elsevier B.V. All rights reserved.