  We consider the problem of incentivising desirable behaviours in multi-agent
systems by way of taxation schemes. Our study employs the concurrent games
model: in this model, each agent is primarily motivated to seek the
satisfaction of a goal, expressed as a Linear Temporal Logic (LTL) formula;
secondarily, agents seek to minimise costs, where costs are imposed based on
the actions taken by agents in different states of the game. In this setting,
we consider an external principal who can influence agents' preferences by
imposing taxes (additional costs) on the actions chosen by agents in different
states. The principal imposes taxation schemes to motivate agents to choose a
course of action that will lead to the satisfaction of their goal, also
expressed as an LTL formula. However, taxation schemes are limited in their
ability to influence agents' preferences: an agent will always prefer to
satisfy its goal rather than otherwise, no matter what the costs. The
fundamental question that we study is whether the principal can impose a
taxation scheme such that, in the resulting game, the principal's goal is
satisfied in at least one or all runs of the game that could arise by agents
choosing to follow game-theoretic equilibrium strategies. We consider two
different types of taxation schemes: in a static scheme, the same tax is
imposed on a state-action profile pair in all circumstances, while in a dynamic
scheme, the principal can choose to vary taxes depending on the circumstances.
We investigate the main game-theoretic properties of this model as well as the
computational complexity of the relevant decision problems.
