Specialization of Interaction Protocols in a Temporal Action Logic

Temporal logics are well suited for the specification and verification of systems of communicating agents. In this paper we adopt a social approach to agent communication, where communication is described in terms of changes to the social state, and interaction protocols in terms of permissions and commitments among agents. In particular, we make use of a temporal action theory, where a protocol is defined as a set of temporal constraints, which specify the effects and preconditions of the communicative actions on the social state. The paper addresses the problem of combining two protocols to define a new more specialized protocol, and presents a notion of protocol specialization which is based on the well known notion of stuttering equivalence between runs. Moreover, the paper studies sufficient conditions (verifiable from the protocol specification) which guarantee that the combination of two protocols is legal.