Verifying and Designing Equilibria in Multiagent Systems
Date:
Verifying equilibria involves checking which temporal logic properties will hold in some “stable” runs of a system composed of multiple agents which are assumed to behave rationally and strategically in pursuit of individual objectives. This paradigm is called rational verification, and can be regarded as a counterpart to (classical) model checking for multi-agent systems. In this talk, I will propose a practically amenable technique for rational verification which relies on a reduction to the solution of a collection of parity games. This approach has been implemented in a tool called EVE. I will also talk about some cases in which the problem of rational verification is computationally tractable. In particular, it is possible to reduce the complexity from 2EXPTIME to fixed-parameter tractable. Finally, I will also introduce a concept called equilibrium design which is concerned in the design of incentives so that a desirable equilibrium is obtained. Extended abstract Slides