2015/04/25 by Natasha Alechina, Brian Logan, Alechina, Natasha +5
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Multiagent Systems (cs.MA)
paper · pdf · doi:10.48550/arxiv.1504.06766
openalex publication_date 2015/04/25 · openalex created_date 2022/09/05 · openalex updated_date 2026/07/28
Several logics for expressing coalitional ability under resource bounds have\nbeen proposed and studied in the literature. Previous work has shown that if\nonly consumption of resources is considered or the total amount of resources\nproduced or consumed on any path in the system is bounded, then the\nmodel-checking problem for several standard logics, such as Resource-Bounded\nCoalition Logic (RB-CL) and Resource-Bounded Alternating-Time Temporal Logic\n(RB-ATL) is decidable. However, for coalition logics with unbounded resource\nproduction and consumption, only some undecidability results are known. In this\npaper, we show that the model-checking problem for RB-ATL with unbounded\nproduction and con- sumption of resources is decidable but EXPSPACE-hard. We\nalso investigate some tractable cases and provide a detailed comparison to a\nvariant of the resource logic RAL, together with new complexity results.\n