SPECIFICATION AND VERIFICATION OF AGENT INTERACTIONS USING SOCIAL INTEGRITY CONSTRAINTS

In this paper we propose a logic-based social approach for specification and verification of agent interaction. We firstly introduce integrity constraints about social acts (called Social Integrity Constraints) as a formalism to express interaction protocols and give a social semantics to the behavior of agents, focusing on communicative acts. Then, we discuss several possible kinds of verification of agent interaction, and we show how social integrity constraints can be used to verify some properties in this respect. We focus our interest on static verification of the compliance of agent specifications to interaction protocols, and on run-time verification, based on agents' observable behavior. We adopt as a running example the NetBill security transaction protocol for the selling and delivery of information goods.