Cooperative Concurrent Games

Rational verification is the problem of determining which temporal logic properties will hold in a multi-agent system, under the assumption that agents in the system act rationally, by choosing strategies that collectively form a game theoretic equilibrium. Previous work in this area has largely focussed on non-cooperative games, with Nash equilibrium and a number of variants as the main game-theoretic solution concepts. Here, we extend the rational verification framework to cooperative games, in which players may form coalitions to collectively achieve their goals, and base our study on the core as our basic solution concept. In particular, we have developed the theory and algorithms for rational verification in both deterministic and probabilistic systems, using concurrent game structures (CGS) and concurrent stochastic games (CSG), respectively, as models. We show that if players’ goals are given by LTL formulae, regardless of the type of solution concept (Nash equilibrium or the core) or underlying model (CGS or CSG), solving such multi-player games can be done in 2EXPTIME, but in each case requiring rather different proof techniques.

Authors

• Julian Gutierrez

Keywords

No keywords are indexed for this paper.