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.
