Symbolic model checking of institutions

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. Categories and S...

• Type: Conference
• Year: 2007
• Where: ACMICEC
• Authors: Francesco Viganò, Marco Colombetti
• Keywords: ACMICEC 2007, Distributed Artificial Intelligence, ECommerce, Model, Model Checking