Model-checking for resource-bounded ATL with production and consumption of resources

DOI10.1016/J.JCSS.2017.03.008MaRDI QIDQ2361350zbMATH OpenOpenAlexFDO

Authors Natasha Alechina, Brian Logan, Hoang Nga Nguyen, Franco Raimondi

Publication date 30 June 2017

Published in Journal of Computer and System Sciences (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1504.06766

zbMATH Keywords

coalitional abilitymodel checkingresourcesverification of multi-agent systems

Mathematics Subject Classification ID

Temporal logic (03B44) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: 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 con- sumption 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.

Recommendations

• Decidable model-checking for a resource logic with production of resources
• On the complexity of resource-bounded logics
• scientific article; zbMATH DE number 7368413
• Logic for coalitions with bounded resources
• Alternating-time temporal logic with resource bounds

Cites work

• Acceleration for Petri nets
• Alternating-time temporal logic
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Decidable model-checking for a resource logic with production of resources
• How to be both rich and happy: combining quantitative and qualitative strategic reasoning about multi-player games (extended abstract)
• scientific article; zbMATH DE number 3885321 (Why is no real title available?)
• Model checking coalitional games in shortage resource scenarios
• Model Checking Logics of Strategic Ability: Complexity*
• On a logic for coalitional games with priced-resource agents
• On the (un-)decidability of model checking resource-bounded agents

Cited in

(16)

• Strategic reasoning with a bounded number of resources: the quest for tractability
• Natural strategic ability
• On a logic for coalitional games with priced-resource agents
• Expressing properties of resource-bounded systems: the logics RTL\(^{*}\) and RTL
• ATL with Strategy Contexts and Bounded Memory
• Alternating-time temporal logic with resource bounds
• Model checking coalitional games in shortage resource scenarios
• scientific article; zbMATH DE number 7368413 (Why is no real title available?)
• State of the Art in Logics for Verification of Resource-Bounded Multi-Agent Systems
• The virtues of idleness: a decidable fragment of resource agent logic
• Decidable model-checking for a resource logic with production of resources
• A public announcement separation logic
• On the complexity of resource-bounded logics
• On the complexity of resource-bounded logics
• Knowing the price of success
• Equilibria for games with combined qualitative and quantitative objectives

Describes a project that uses

Uses Software

• MCMAS

This page was built for publication: Model-checking for resource-bounded ATL with production and consumption of resources

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2361350)