Norm-based mechanism design

In this paper, we first introduce a formal setting of multi-agent environments based on concurrent game structures which abstracts from concrete specification languages. We extend this formal setting with norms and sanctions, and show how concepts from mechanism design can be used to formally analyse and verify whether a specific behaviour can be enforced (or implemented) if agents follow their subjective preferences. We relate concepts from mechanism design to our setting, where agents' preferences are modelled by linear time temporal logic (LTL) formulae. This proposal bridges the gap between norms and mechanism design allowing us to formally study and analyse the effect of norms and sanctions on the behaviour of rational agents. The proposed machinery can be used to check whether specific norms and sanctions have the designer's expected effect on the rational agents' behaviour or if a set of norms and sanctions that realise the effect exists at all. We investigate the computational complexity of our framework, focusing on its implementation in Nash equilibria and we show that it is located at the second and third level of the polynomial hierarchy. Despite this high complexity, on the positive side, these results are in line with existing complexity results of related problems. Finally, we propose a concrete executable specification language that can be used to implement multi-agent environments. We show that the proposed specification language generates specific concurrent game structures and that the abstract multi-agent environment setting can be applied to study and analyse the behaviour of multi-agent programs with and without norms.