Resource-bounded alternating-time temporal logic

Many problems in AI and multi-agent systems research are mostnaturally formulated in terms of the abilities of a coalition of agents. There exist several excellent logical tools for reasoning about coalitional ability. However, coalitional ability can be affected by theavailability of resources, and there is no straightforward way ofreasoning about resource requirements in logics such as CoalitionLogic (CL) and Alternating-time Temporal Logic (ATL). In thispaper, we propose a logic for reasoning about coalitional abilityunder resource constraints. We extend ATL with costs of actionsand hence of strategies. We give a complete and sound axiomatisation of the resulting logic Resource-Bounded ATL (RB-ATL) andan efficient model-checking algorithm for it.

Authors

• Natasha Alechina
• Brian Logan
• Hoang Nga Nguyen
• Abdur Rakib

Keywords

• Logics for agency
• Verification of MAS