A Framework for Model Checking Institutions

  • Francesco Viganò
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4428)


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.


Model Check Status Function Multiagent System Atomic Proposition Valuation Function 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, Springer, Heidelberg (2002)CrossRefGoogle Scholar
  2. 2.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambrige, MA (1999)Google Scholar
  3. 3.
    Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: Predicate Abstraction of ANSI-C Programs Using SAT. Formal Methods in System Design 25(2-3), 105–127 (2004)zbMATHCrossRefGoogle Scholar
  4. 4.
    Cliffe, O., Padget, J.: A Framework For Checking Interactions Within Agent Institutions. In: Proceedings of the ECAI Workshop on Model Checking and Artificial Intelligence (MoChart I) (2002)Google Scholar
  5. 5.
    Cliffe, O., Vos, M.D., Padget, J.: Specifying and Analysing Agent-based Social Institutions using Answer Set Programming. In: Boissier, O., Padget, J., Dignum, V., Lindemann, G., Matson, E., Ossowski, S., Sichman, J.S., Vázquez-Salceda, J. (eds.) Coordination, Organizations, Institutions, and Norms in Multi-Agent Systems. LNCS (LNAI), vol. 3913, pp. 99–113. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communication of the ACM 18(8), 453–457 (1975)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Esteva, M., de la Cruz, D., Sierra, C.: ISLANDER: an electronic institutions editor. In: Castelfranchi, C., Johnson, W.L. (eds.) Proceedings of the first international joint conference on Autonomous Agents and Multiagent Systems (AAMAS 2002), pp. 1045–1052. ACM Press, New York (2002)CrossRefGoogle Scholar
  8. 8.
    Esteva, M., Rodríguez-Aguilar, J.A., Sierra, C., Garcia, P., Arcos, J.L.: On the Formal Specification of Electronic Institutions. In: Dignum, F., Sierra, C. (eds.) Agent Mediated Electronic Commerce. LNCS (LNAI), vol. 1991, pp. 126–147. Springer, Heidelberg (2001)Google Scholar
  9. 9.
    Fornara, N., Viganò, F., Colombetti, M.: Agent Communication and Institutional Reality. In: van Eijk, R.M., Huget, M.-P., Dignum, F.P.M. (eds.) AC 2004. LNCS (LNAI), vol. 3396, pp. 1–17. Springer, Heidelberg (2005)Google Scholar
  10. 10.
    García-Camino, A., Rodríguez-Aguilar, J.A., Sierra, C., Vasconcelos, W.W.: A distributed architecture for norm-aware agent societies. In: Baldoni, M., Endriss, U., Omicini, A., Torroni, P. (eds.) DALT 2005. LNCS (LNAI), vol. 3904, pp. 89–105. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  11. 11.
    Graf, S., Saidi, H.: Construction of Abstract State Graphs with PVS. In: Proceedings of the 9th International Conference on Computer Aided Verification, pp. 72–83. Springer, Heidelberg (1997)Google Scholar
  12. 12.
    Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, London (2003)Google Scholar
  13. 13.
    Huget, M.-P., Esteva, M., Phelps, S., Sierra, C., Wooldridge, M.: Model Checking Electronic Institutions. In: Proceedings of the ECAI Workshop on Model Checking and Artificial Intelligence (MoChArt I) (2002)Google Scholar
  14. 14.
    Jones, A., Sergot, M.J.: A formal characterisation of institutionalised power. Journal of the IGPL 4(3), 429–445 (1996)MathSciNetGoogle Scholar
  15. 15.
    Kowalski, R.A., Sergot, M.J.: A Logic-based Calculus of Events. New Generation Computing 4, 67–95 (1986)CrossRefGoogle Scholar
  16. 16.
    Lomuscio, A., Sergot, M.: A formulation of violation, error recovery, and enforcement in the bit transmission problem. Journal of Applied Logic (Selected articles from DEON02 - London) 1(2), 93–116 (2002)Google Scholar
  17. 17.
    Masolo, C., Vieu, L., Bottazzi, E., Catenacci, C., Ferrario, R., Gangemi, A., Guarino, N.: Social Roles and their Descriptions. In: Dubois, D., Welty, C., Williams, M. (eds.) Proceedings of the Ninth International Conference on the Principles of Knowledge Representation and Reasoning (KR2004), pp. 267–277 (2004)Google Scholar
  18. 18.
    Meinke, K., Tucker, J.V. (eds.): Many-sorted logic and its applications. John Wiley & Sons, Inc, New York (1993)zbMATHGoogle Scholar
  19. 19.
    Morzenti, A., Mandrioli, D., Ghezzi, C.: A Model Parametric Real-Time Logic. ACM Transactions on Programming Languages and Systems 14(4), 521–573 (1992)CrossRefGoogle Scholar
  20. 20.
    Moses, Y., Tennenholtz, M.: Artificial Social Systems. Computers and AI 14(6), 533–562 (1995)MathSciNetGoogle Scholar
  21. 21.
    Ostroff, J.S.: Deciding properties of timed transition models. IEEE Transactions on Parallel Distributed Systems 1(2), 170–183 (1990)CrossRefGoogle Scholar
  22. 22.
    Pitt, J., Kamara, L., Sergot, M., Artikis, A.: Formalization of a voting protocol for virtual organizations. In: Proceedings of the 4th International Joint Conference on Autonomous agents and Multi-Agent Systems (AAMAS 2005), pp. 373–380. ACM Press, New York (2005)CrossRefGoogle Scholar
  23. 23.
    Searle, J.R.: The construction of social reality. Free Press, New York, USA (1995)Google Scholar
  24. 24.
    Sergot, M.J.: Modelling unreliable and untrustworthy agent behaviour. In: Dunin-Keplicz, B., Jankowski, A., Skowron, A., Szczuka, M. (eds.) Monitoring, Security, and Rescue Techniques in Multiagent Systems, Advances in Soft Computing, pp. 161–178. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  25. 25.
    Vasconcelos, W.: Logic-based electronic institutions. In: Leite, J.A., Omicini, A., Sterling, L., Torroni, P. (eds.) DALT 2003. LNCS (LNAI), vol. 2990, pp. 221–242. Springer, Heidelberg (2003)Google Scholar
  26. 26.
    Viganò, F.: FIEVeL, a Language for the Specification and Verification of Institutions. Technical Report 3, Institute for Communication Technologies, Università della Svizzera Italiana (2006)Google Scholar
  27. 27.
    Viganò, F., Colombetti, M.: Specification and Verification of Institutions through Status Functions. In: Proceedings of the AAMAS Workshop on Coordination, Organization, Institutions and Norms in agent systems (COIN 2006) (2006)Google Scholar
  28. 28.
    Walton, C.D.: Model Checking Agent Dialogues. In: Leite, J.A., Omicini, A., Torroni, P., Yolum, P. (eds.) DALT 2004. LNCS (LNAI), vol. 3476, pp. 132–147. Springer, Heidelberg (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Francesco Viganò
    • 1
  1. 1.Università della Svizzera italiana, via G. Buffi 13, 6900 LuganoSwitzerland

Personalised recommendations