Model-checking for Resource-Bounded ATL with production and consumption of resources
Model-checking for Resource-Bounded ATL with production and consumption of resources
复制标题
具有资源生产和消耗的资源有限 ATL 的模型检查
DOI：
10.1016/j.jcss.2017.03.008
复制
发表时间：
2017
影响因子：
1.1
通讯作者：
Alechina N
中科院分区：
文献类型：
--
作者：
Alechina N
文献中已经提出并研究了几种表示资源约束下联盟能力的逻辑。已有的工作表明，如果只考虑资源消耗，或者系统中任意路径上产生或消耗的资源总量是有界的，那么几种标准逻辑，如资源有界联合逻辑（RB-CL）和资源有界交替时序逻辑（RB-ATL）的模型检测问题是可判定的.然而，对于具有无限资源生产和消费的联盟逻辑，只知道一些不可判定性结果。在本文中，我们证明了RB-ATL的模型检测问题的无限生产和消费的资源是可判定的，但EXPSPACE困难。我们还调查了一些易于处理的情况下，并提供了一个详细的比较，资源逻辑RAL的一个变种，连同新的复杂性结果。
Several logics for expressing coalitional ability under resource bounds have been proposed and studied in the literature. Previous work has shown that if only consumption of resources is considered or the total amount of resources produced or consumed on any path in the system is bounded, then the model-checking problem for several standard logics, such as Resource-Bounded Coalition Logic (RB-CL) and Resource-Bounded Alternating-Time Temporal Logic (RB-ATL) is decidable. However, for coalition logics with unbounded resource production and consumption, only some undecidability results are known. In this paper, we show that the model-checking problem for RB-ATL with unbounded production and consumption of resources is decidable but EXPSPACE-hard. We also investigate some tractable cases and provide a detailed comparison to a variant of the resource logic RAL, together with new complexity results.
登录
查看更多内容
Petri 网的加速
影响因子：
0.4
作者：
Jérôme Leroux
通讯作者：
Jérôme Leroux
资源短缺场景下联盟博弈的模型检验
DOI：
10.4204/eptcs.119.20
发表时间：
2013
期刊：
The Journal of experimental medicine
影响因子：
--
作者：
Dario Della Monica;M. Napoli;Mimmo Parente
通讯作者：
Mimmo Parente
可判定的模型检查与资源生产的资源逻辑
DOI：
10.3233/978-1-61499-419-0-9
发表时间：
2014
期刊：
ECAI 2014 - 21st European Conference on Artificial Intelligence
影响因子：
--
作者：
Alechina, N
通讯作者：
Alechina, N
如何既富有又快乐：定量与定性相结合的多人游戏战略推理（扩展摘要）
影响因子：
--
作者：
N. Bulling;V. Goranko
通讯作者：
V. Goranko