Efficient Verification of MASs with Projections

Abstract. Constrained global types are a powerful means to represent agent interaction protocols. In our recent research we used them to rep-resent complex protocols in a very compact way, and we exploited them to dynamically verify actual agents ’ interactions with respect to different protocols in both Jason and JADE. The main drawback of our previous approach is the full centralization of the monitoring activity, which is del-egated to a unique monitor agent in charge of verifying that the messages exchanged among all the agents are compliant with the protocol. This approach works well for MASs with few agents, but could become un-suitable in communication-intensive and highly-distributed MASs where hundreds of agents should be monitored. In this paper we define an algorithm for projecting a constrained global type onto a set of agents Ags, by restricting it to the interactions in-volving agents in Ags, so that the outcome of the algorithm is another constrained global type where interactions involve only agents in Ags. The projection mechanism is the first step towards distributing the mon-itoring activity, making it safer and more efficient: the compliance of a MAS to a protocol could be dynamically verified by suitably partition-ing the agents of the MAS into small sets of agents, and by assigning to each partition Ags a local monitor agent which checks all interactions involving Ags against the projected constrained global type. Although the projection of well formed constrained global types can be always performed, the resulting projected protocol does not always model all the constraints as the original one. We describe a generate and test algorithm that provides hints on the correctness of the protocol distri-bution, leaving for further investigation the formal characterization of which protocols can be distributed onto which agents ’ subsets