Animated specifications of computational societies

Abstract

E-markets and negotiation protocols are two types of application domains that can be viewed as open computational societies. Key characteristics of such societies are agent heterogeneity, conflicting individual goals and limited trust. The risk that members of such societies will not conform to specifications imposes the need for a framework that will facilitate the designers to determine to what extent it is desirable to deploy their agents in such societies. We address this need by presenting a formal framework for specifying, animating, and ultimately reasoning about and verifying the properties of open computational systems. We view computational systems from an external perspective, aiming to account for the institutional and social aspects of these systems. We identify the key concepts and illustrate how they are used by formalising an example employing the contract net protocol. The framework and associated logical inferences have been implemented as a software platform that provides automated animation of the global states of an open system (society) during its execution. Simulations have demonstrated that the implementation of the framework establishes a foundation for a rich, formal representation of open computational societies.