  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
explore the concept of equilibrium design, where incentives are designed to
obtain a desirable equilibrium that satisfies a specific temporal logic
property. Our study is based 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. We consider system
specifications given by LTL and GR(1) formulae, and show that designing
incentives to ensure that a given temporal logic property is satisfied on
some/every Nash equilibrium of the game can be achieved in PSPACE for LTL
properties and in NP/{\Sigma}P 2 for GR(1) specifications. We also examine the
complexity of related decision and optimisation problems, such as optimality
and uniqueness of solutions, as well as considering social welfare, and show
that the complexities of these problems lie within the polynomial hierarchy.
Equilibrium design can be used as an alternative solution to rational synthesis
and verification problems for concurrent games with mean-payoff objectives when
no solution exists or as a technique to repair concurrent games with
undesirable Nash equilibria in an optimal way.
