Constrained global types for dynamic checking of protocol conformance in multi-agent systems

Global types are behavioral types for specifying and verifying multiparty interactions between distributed components, inspired by the process algebra approach. In this paper we extend the formalism of global types in multi-agent systems resulted from our previous work with a mechanism for easily expressing constrained shue of message sequences; accordingly, we extend the semantics to include the newly introduced feature, and show the expressive power of these constrained global types"