Attribute Global Types for Dynamic Checking of Protocols in Logic-based Multiagent Systems

This paper introduces Attribute Global Types, an extension inspired by Attribute Grammars to a formalism we have recently proposed for specifying and dynamically verifying multi-party agent interaction protocols. Global types equipped with attributes are more expressive, since they allow parametric specifications of protocols, but despite their expressive power, they can be still effectively used for dynamic checking of protocols: Attribute Global Types can be easily represented as Prolog terms, and a mechanism for verifying that a sequence of messages complies to an Attribute Global Type has been designed and implemented in Prolog. This logic-based representation and implementation allow us to integrate a monitor agent implementing a run-time verification mechanism of protocol compliance into any logic-based agent oriented programming language that supports the basic Prolog built-ins.