Model Checking and Strategy Synthesis for Multi-agent Systems for Resource Allocation

We present a technique for verifying strategic abilities of multi-agent systems via SAT-based bounded model checking. In our approach we focus on systems of agents that pursue goals with regard to the allocation of shared resources. The problem to be solved is to determine whether a coalition of agents has a joint strategy that guarantees the achievement of all resource goals, irrespective of how the opposing agents in the system act. Our approach does not only decide whether such a strategy exists, but also synthesises the strategy. The technique is based on a propositional logic encoding of the model checking problem. The encoding is satisfiable if and only if some specified coalition of agents has a strategy to reach a resource allocation goal. Each satisfying truth assignment of the encoding characterises a successful strategy.