Model Checking Norms and Sanctions in Institutions

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


In this paper we enrich FIEVeL (a modelling language for institutions amenable to model checking) with new constructs to describe norms and sanctions. Moreover, we present a specification language to reason about the effectiveness of norms and sanctions in shaping agent interactions. Finally we show that when properties of artificial institutions reflect certain interpretations of norms of human institutions, it is not always possible to satisfy them. As a consequence, regimentation of norms is not always a viable solution.


Model Check Status Function Temporal Logic Normative System Atomic Formula 
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.
    Ågotnes, T., van der Hoek, W., Rodríguez-Aguilar, J.A., Sierra, C., Wooldridge, M.: On the logic of normative systems. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence, pp. 1175–1180 (2007)Google Scholar
  2. 2.
    Artikis, A., Kamara, L., Pitt, J., Sergot, M.J.: A Protocol for Resource Sharing in Norm-Governed Ad Hoc Networks. In: Leite, J.A., Omicini, A., Torroni, P., Yolum, p. (eds.) DALT 2004. LNCS (LNAI), vol. 3476, pp. 221–238. Springer, Heidelberg (2005)Google Scholar
  3. 3.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  4. 4.
    Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. Journal of the ACM 33(1), 151–178 (1986)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Esteva, M., Rodríguez-Aguilar, J.A., Sierra, C., Garcia, P., Arcos, J.L.: On the Formal Specification of Electronic Institutions. In: Sierra, C., Dignum, F.P.M. (eds.) AgentLink 2000. LNCS (LNAI), vol. 1991, pp. 126–147. Springer, Heidelberg (2001)Google Scholar
  6. 6.
    Fornara, N., Colombetti, M.: Specifying and Enforcing Norms in Artificial Institutions. In: Omicini, A., Dunin-Keplicz, B., Padget, J. (eds.) Proceedings of the 4th European Workshop on Multi-Agent Systems (2006)Google Scholar
  7. 7.
    Fornara, N., Viganò, F., Colombetti, M.: Agent Communication and Artificial Institutions. Autonomous Agents and Multi-Agent Systems 14(2), 121–142 (2007)CrossRefGoogle Scholar
  8. 8.
    García-Camino, A.: Ignoring, Forcing and Expecting Concurrent Events in Electronic Institutions. In: Sichman, J.S., et al. (eds.) COIN 2007 Workshops. LNCS (LNAI), vol. 4870, pp. 316–329. Springer, Heidelberg (2008)Google Scholar
  9. 9.
    Grossi, D., Aldewereld, H., Dignum, F.: Ubi lex, ibi poena: Designing norm enforcement in e-institutions. In: Noriega, P., Vázquez-Salceda, J., Boella, G., Boissier, O., Dignum, V., Fornara, N., Matson, E. (eds.) COIN 2006, vol. 4386, pp. 110–124. Springer, Heidelberg (2007)Google Scholar
  10. 10.
    Jones, A., Sergot, M.J.: On the characterization of law and computer systems: The normative systems perspectives. In: Deontic Logic in Computer Science: Normative Systems Specification, pp. 275–307 (1993)Google Scholar
  11. 11.
    Jones, A., Sergot, M.J.: A formal characterisation of institutionalised power. Journal of the IGPL 4(3), 429–445 (1996)MathSciNetGoogle Scholar
  12. 12.
    Lomuscio, A., Sergot, M.: A formulation of violation, error recovery, and enforcement in the bit transmission problem. Journal of Applied Logic 1(2), 93–116 (2002)MathSciNetGoogle Scholar
  13. 13.
    Manzano, M.: Introduction to many-sorted logic. In: Many-sorted logic and its applications, pp. 3–86. John Wiley, Chichester (1993)Google Scholar
  14. 14.
    Meyer, J.-J., Wieringa, R.J.: Deontic Logic: A Concise Overview. In: Deontic Logic in Computer Science: Normative Systems Specification, pp. 3–16. John Wiley, Chichester (1993)Google Scholar
  15. 15.
    Pitt, J., Kamara, L., Sergot, M., Artikis, A.: Formalization of a voting protocol for virtual organizations. In: Proceedings of the 4th Conference on Autonomous agents and Multi-Agent Systems, pp. 373–380 (2005)Google Scholar
  16. 16.
    Raimondi, F., Lomuscio, A.: Automatic Verification of Deontic Interpreted Systems by Model Checking via OBDD’s. In: Proceedings of the 16th European Conference on Artificial Intelligence, pp. 53–57 (2004)Google Scholar
  17. 17.
    Searle, J.R.: The construction of social reality. Free Press, New York (1995)Google Scholar
  18. 18.
    Sergot, M.J., Craven, R.: The Deontic Component of Action Language nC+. In: Goble, L., Meyer, J.-J.C. (eds.) DEON 2006. LNCS (LNAI), vol. 4048, pp. 222–237. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  19. 19.
    Viganò, F., Colombetti, M.: Specification and Verification of Institutions through Status Functions. In: Noriega, P., et al. (eds.) COIN 2006. LNCS (LNAI), vol. 4386, pp. 125–141. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  20. 20.
    Viganò, F., Colombetti, M.: Symbolic Model Checking of Institutions. In: Proceedings of the 9th International Conference on Electronic Commerce (ICEC 2007), pp. 35–44. ACM Press (2007)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Francesco Viganò
    • 1
  • Marco Colombetti
    • 1
    • 2
  1. 1.Università della Svizzera italianaLuganoSwitzerland
  2. 2.Politecnico di MilanoMilanoItaly

Personalised recommendations