A framework for model checking institutions

To increase positive expectations in the outcome of open multiagent systems, institutions have been put forward to regulate agents' behaviour. To model and to verify such institutions, we propose to adopt the notion of status function, which provides for a unified approach to ontological and deontic aspects regulated by an institution. Also, to enhance the development of functional and rational institutions, we propose a language amenable to model checking to describe them and their properties. Finally, we present our tool and an evaluation of our approach.