Game specification in normative multiagent system: the trias politica

In this paper we formalize the specification of games in the trias politica using Rao and Georgeff's specification language BDI{CTL}. In particular, we generalize Rao and Georgeff's specification of single agent decision trees to multiagent games, for which we introduce observations and recursive modelling, in this setting we formalize obligations, and we characterize four kinds of agents, called legislators, judges, policemen and citizens. Legislators are characterized by their power to create and revise obligations, judges are characterized by their power to count behavior of citizens as violations, and policemen are characterized by their ability to sanction behavior.