Cooperative Concurrent Games
Julian Gutierrez, Szymon Kowara, Sarit Kraus, Thomas Steeples, Michael, Wooldridge

TL;DR
This paper extends rational verification to cooperative game theory, focusing on the core concept, analyzing its computational complexity, and exploring conditions for non-emptiness and invariance, with applications to mean-payoff preferences.
Contribution
It introduces a variant of the core for concurrent games, characterizes it with ATL*, and studies its computational complexity and properties under different preference models.
Findings
Core variant characterized by ATL*
Complexity ranges from PSPACE to 3EXPTIME
Conditions for core non-emptiness and invariance
Abstract
In rational verification, the aim is to verify which temporal logic properties will obtain in a multi-agent system, under the assumption that agents ("players") in the system choose strategies for acting that form a game theoretic equilibrium. Preferences are typically defined by assuming that agents act in pursuit of individual goals, specified as temporal logic formulae. To date, rational verification has been studied using non-cooperative solution concepts - Nash equilibrium and refinements thereof. Such non-cooperative solution concepts assume that there is no possibility of agents forming binding agreements to cooperate, and as such they are restricted in their applicability. In this article, we extend rational verification to cooperative solution concepts, as studied in the field of cooperative game theory. We focus on the core, as this is the most fundamental (and most widely…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
