Efficient verification of MASs with projections

Constrained global types are a powerful means to represent agent interaction protocols. In our recent research we demonstrated that they can be used to represent complex protocols in a very compact way, and we exploited them to dynamically verify the correct implementation of a protocol in two real MAS frameworks, Jason and JADE. The main drawback of our previous approach is the full centralization of the monitoring activity, which is delegated to a unique monitor agent. This approach works well for MASs with few agents, but could become unsuitable 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 involving agents in Ags, so that the outcome of the algorithm is another constrained global type that can be safely used for verifying the compliance of the sub-system Ags to the protocol specified by the original constrained global type. The projection mechanism is the first step towards distributing the monitoring activity, making it safer and more efficient: the compliance of a MAS to a protocol could be dynamically verified by suitably partitioning 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 distribution, leaving for further investigation the formal characterization of which protocols can be distributed onto which agents’ subsets.