Model checking coalitional games in shortage resource scenarios
Model checking coalitional games in shortage resource scenarios
复制标题
资源短缺场景下联盟博弈的模型检验
DOI：
10.4204/eptcs.119.20
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Mimmo Parente
中科院分区：
文献类型：
--
作者：
Dario Della Monica;M. Napoli;Mimmo Parente
多智能体系统（MAS）的验证已被研究，考虑到需要表达的资源界限。几个逻辑指定属性的MAS已经提出了相当多种方案与有限的资源。在本文中，我们研究了一种不同的形式主义，称为定价资源有界交替时间时序逻辑（PRBATL），其主要的新奇在于移动的概念，资源从语法层面（部分公式）的语义（部分模型）。这使我们能够跟踪资源可用性沿着计算的演变，并为我们提供了一个能够模拟许多真实世界场景的形式主义。两个相关方面是市场上资源的全球可用性（由代理人共享）的概念，以及资源价格（取决于其可用性）的概念。在我们以前的工作中，对这种新的形式主义的第一步介绍，沿着与EXPTIME算法的模型检测问题。在本文中，我们更好地分析所提出的形式主义的特点，也与以前的方法相比。主要的技术贡献是证明的EXPTIME硬度的模型检查问题PRBATL的基础上，减少从接受问题的线性有界交替图灵机。特别是，由于该问题有多个参数，我们显示了两个固定参数的减少。
Verification of multi-agents systems (MAS) has been recently studied taking into account the need of expressing resource bounds. Several logics for specifying properties of MAS have been presented in quite a variety of scenarios with bounded resources. In this paper, we study a different formalism, called Priced Resource-Bounded Alternating-time Temporal Logic (PRBATL), whose main novelty consists in moving the notion of resources from a syntactic level (part of the formula) to a semantic one (part of the model). This allows us to track the evolution of the resource availability along the computations and provides us with a formalisms capable to model a number of real-world scenarios. Two relevant aspects are the notion of global availability of the resources on the market, that are shared by the agents, and the notion of price of resources, depending on their availability. In a previous work of ours, an initial step towards this new formalism was introduced, along with an EXPTIME algorithm for the model checking problem. In this paper we better analyze the features of the proposed formalism, also in comparison with previous approaches. The main technical contribution is the proof of the EXPTIME-hardness of the the model checking problem for PRBATL, based on a reduction from the acceptance problem for Linearly-Bounded Alternating Turing Machines. In particular, since the problem has multiple parameters, we show two fixed-parameter reductions.