Nash equilibria in generalised dining philosophers games

Abstract

The Generalised Dining Philosophers Game (GDPG) consists of agents which must cooperate (or compete) for shared resources. As there are several cooperating agents, we can think of the GDPG as a multi-agent system. In such a system, there are naturally some qualitative objectives such as fairness and liveness; and quantitative objectives where the agents seek to satisfy their goal as frequently as possible. The GDPG is represented as a concurrent game model and the agents’ objectives are represented by LTL[F] formulas. There are some qualitative objectives which represent the goals of the entire group, and some quantitative objectives which represent the individual agents’ and should be optimised. From this point, the LTL[F] model checking procedure is modified to produce an automaton-based algorithm which identifies a strategy profile which satisfies the qualitative objectives, and also is a Nash Equilibrium with respect to the agent’s quantitative objectives. That is, at each configuration of the game, an action must be prescribed to each agent such that the collective objectives of the group are satisfied, and no agent can unilaterally deviate in order to achieve a better outcome.