Concurrent multi-player mean-payoff games serve as important models for
multi-agent systems with quantitative individual goals. These games have
been extensively studied in non-cooperative settings, for example, using
Nash equilibrium. This talk, however, explores an alternative setting:
what happens if cooperation is possible? This setting is particularly
relevant for cooperative AI systems, as it allows for the modelling of
cooperation among agents, even when their goals do not fully align.
First, we present a characterisation of cooperative game solution
concept called the core using discrete geometry techniques and establish
a necessary and sufficient condition for its non-emptiness. Second, we
utilise this characterisation to demonstrate the existence of polynomial
witnesses in the core. Finally, we leverage this existence to address
key decision problems in rational verification.
29/02/2024