Symbolic model checking of institutions

ABSTRACT

Norms defined by institutions and enforced by organizations have been put forward as a mechanism to increase the efficiency and reliability of electronic transactions carried out by agents in open systems. Despite several approaches have been proposed to model protocols in terms of institutional concepts (e.g., obligations and powers) and to monitor the actual compliance of agents' behavior at runtime, little work has been done to formally guarantee that such systems of norms ensure certain desirable properties. In this paper we describe a framework to verify institutions, which is characterized by a metamodel of institutional reality, languages to describe institutions and to specify their properties, and a tool to model check them. Finally, to evaluate our approach, we model and verify the Dutch Auction institution, a widely used interaction protocol, showing that the verification of institutional rules constitutes a necessary step to define sound institutions.

REFERENCES

• 1: Martín Abadi, The power of temporal proofs, Theoretical Computer Science, v.65 n.1, p.35-83, 15 June 1989 [doi>10.1016/0304-3975(89)90138-2]
• 2: Patrick Blackburn , Maarten de Rijke , Yde Venema, Modal logic, Cambridge University Press, New York, NY, 2001
• 3: G. Boella and L. van der Torre. The Ontological Properties of Social Roles: Definitional Dependence, Powers and Roles Playing Roles. In Proceedings of the Workshop on Legal Ontologies and Artificial Intelligence Techniques, 2005.
• 4: Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]
• 5: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 6: O. Cliffe and J. Padget. A Framework For Checking Interactions Within Agent Institutions. In Proceedings of the ECAI Workshop on Model Checking and Artificial Intelligence, 2002.
• 7: O. Cliffe, M. D. Vos, and J. Padget. Specifying and Analysing Agent-based Social Institutions using Answer Set Programming. In Coordination, Organization, Institutions, and Norms in Multi-Agent Systems, volume 3913 of LNAI, pages 99--113. Springer, 2006.
• 8: S. Cranefield. Modelling and Monitoring Social Expectations in Multi-Agent Systems. In Coordination, Organizations, Institutions, and Norms in Multi-Agent Systems II, volume 4386 of LNCS, 2007.
• 9: N. E&3233;n and N. Sörensson. An Extensible SAT-solver. In Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing., volume 2919 of LNCS, pages 502--518. Springer, 2004.
• 10: E. Allen Emerson , Joseph Y. Halpern, “Sometimes” and “not never” revisited: on branching versus linear time temporal logic, Journal of the ACM (JACM), v.33 n.1, p.151-178, Jan. 1986 [doi>10.1145/4904.4999]
• 11: Marc Esteva , David de la Cruz , Carles Sierra, ISLANDER: an electronic institutions editor, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 3, July 15-19, 2002, Bologna, Italy [doi>10.1145/545056.545069]
• 12: Marc Esteva , Bruno Rosell , Juan A. Rodriguez-Aguilar , Josep Ll. Arcos, AMELI: An Agent-Based Middleware for Electronic Institutions, Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems, p.236-243, July 19-23, 2004, New York, New York [doi>10.1109/AAMAS.2004.56]
• 13: Marc Esteva , Juan A. Rodríguez-Aguilar , Carles Sierra , Pere Garcia , Josep Lluís Arcos, On the Formal Specifications of Electronic Institutions, Agent Mediated Electronic Commerce, The European AgentLink Perspective., p.126-147, January 2001
• 14: M. Esteva, J. A. Rodríguez-Aguilar, C. Sierra, and W. Vasconcelos. Verifying Norm Consistency in Electronic Institutions. In Proceedings of the Workshop on Agent Organizations: Theory and Practice, pages 8--15, 2004.
• 15: Nicoletta Fornara , Francesco Viganò , Marco Colombetti, Agent communication and artificial institutions, Autonomous Agents and Multi-Agent Systems, v.14 n.2, p.121-142, April 2007 [doi>10.1007/s10458-006-0017-8]
• 16: A. García-Camino , J. A. Rodríguez-Aguilar , C. Sierra , W. Vasconcelos, A rule-based approach to norm-oriented programming of electronic institutions, ACM SIGecom Exchanges, v.5 n.5, p.33-40, January 2006 [doi>10.1145/1124566.1124571]
• 17: G. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison Wesley, 2003.
• 18: M.-P. Huget, M. Esteva, S. Phelps, C. Sierra, and M. Wooldridge. Model Checking Electronic Institutions. In Proceedings of the ECAI Workshop on Model Checking and Artificial Intelligence, 2002.
• 19: A. Jones and M. J. Sergot. A formal characterisation of institutionalised power. Journal of the IGPL, 4(3):429--445, 1996.
• 20: Anneke G. Kleppe , Jos Warmer , Wim Bast, MDA Explained: The Model Driven Architecture: Practice and Promise, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2003
• 21: María Manzano, Introduction to many-sorted logic, Many-sorted logic and its applications, John Wiley & Sons, Inc., New York, NY, 1993
• 22: C. Masolo, L. Vieu, E. Bottazzi, C. Catenacci, R. Ferrario, A. Gangemi, and N. Guarino. Social Roles and their Descriptions. In Proceedings of the International Conference on the Principles of Knowledge Representation and Reasoning, pages 267--277, 2004.
• 23: Kenneth L. McMillan, Applying SAT Methods in Unbounded Symbolic Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.250-264, July 27-31, 2002
• 24: Y. Moses and M. Tennenholtz. Artificial Social Systems. Computers and AI, 14(6):533--562, 1995.
• 25: P. Noriega. Agent mediated auctions: The Fishmarket Metaphor. PhD thesis, Universitat Autònoma de Barcelona, 1997.
• 26: D. North. Institutions, Institutional Change and Economics Performance. Cambridge University Press, 1990.
• 27: Doron A. Peled , David Gries , Fred B. Schneider, Software reliability methods, Springer-Verlag New York, Inc., Secaucus, NJ, 2001
• 28: Jeremy Pitt , Lloyd Kamara , Marek Sergot , Alexander Artikis, Formalization of a voting protocol for virtual organizations, Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems, July 25-29, 2005, The Netherlands [doi>10.1145/1082473.1082530]
• 29: F. Raimondi and A. Lomuscio. Automatic verification of deontic interpreted systems by model checking via obdd's. In Proceedings of the 16th Eureopean Conference on Artificial Intelligence, pages 53--57, 2004.
• 30: J. R. Searle. The construction of social reality. Free Press, 1995.
• 31: J. R. Searle. What is an institution? Journal of Institutional Economics, 1(01):1--22, 2005.
• 32: D. Sheridan. The optimality of a fast cnf conversion and its use with sat. In The 7th International Conference on Theory and Applications of Satisfiability Testing, 2004.
• 33: F. Somenzi. CUDD: CU Decision Diagram Package. http://vlsi.colorado.edu/~fabio/CUDD/.
• 34: W. Vasconcelos. Logic-Based Electronic Institutions. In Proceedings of the Workshop on Declarative Agent Languages and Technologies, volume 2990 of LNCS, pages 221--242. Springer, 2004.
• 35: J. Vázquez-Salceda, H. Aldewereld, and F. Dignum. Norms in Multiagent Systems: from Theory to Practice. International Journal of Computer Systems Science & Engineering, 20(4):225--236, 2005.
• 36: F. Viganò and M. Colombetti. Specification and Verification of Institutions through Status Functions. In Coordination, Organizations, Institutions, and Norms in Multi-Agent Systems II, volume 4386 of LNCS, 2007.
• 37: F. Viganè, N. Fornara, and M. Colombetti. An Event Driven Approach to Norms in Artificial Institutions. In Coordination, Organization, Institutions, and Norms in Multi-Agent Systems, volume 3913 of LNAI, pages 142--154. Springer, 2006.
• 38: M. Wooldridge, M. -P. Huget, M. Fisher, and S. Parsons. Model Checking for Multiagent Systems: the Mable Language and its Applications. International Journal on Artificial Intelligence Tools, 15(2):195--226, 2006.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
        I.2.11 Distributed Artificial Intelligence
            Subjects: Multiagent systems

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
        I.2.11 Distributed Artificial Intelligence
            Subjects: Languages and structures

General Terms:
Verification

Keywords:
institutions, model checking, norms