  In game theory, mechanism design is concerned with the design of incentives
so that a desired outcome of the game can be achieved. In this paper, we study
the design of incentives so that a desirable equilibrium is obtained, for
instance, an equilibrium satisfying a given temporal logic property -- a
problem that we call equilibrium design. We base our study on a framework where
system specifications are represented as temporal logic formulae, games as
quantitative concurrent game structures, and players' goals as mean-payoff
objectives. In particular, we consider system specifications given by LTL and
GR(1) formulae, and show that implementing a mechanism to ensure that a given
temporal logic property is satisfied on some/every Nash equilibrium of the
game, whenever such a mechanism exists, can be done in PSPACE for LTL
properties and in NP/$\Sigma^{P}_{2}$ for GR(1) specifications. We also study
the complexity of various related decision and optimisation problems, such as
optimality and uniqueness of solutions, and show that the complexities of all
such problems lie within the polynomial hierarchy. As an application,
equilibrium design can be used as an alternative solution to the rational
synthesis and verification problems for concurrent games with mean-payoff
objectives whenever no solution exists, or as a technique to repair, whenever
possible, concurrent games with undesirable rational outcomes (Nash equilibria)
in an optimal way.
