Specifying and verifying interaction protocols in a temporal action logic

In this paper we develop a logical framework for specifying and verifying systems of communicating agents and interaction protocols. The framework is based on Dynamic Linear Time Temporal Logic (DLTL), which extends LTL by strengthening the until operator by indexing it with the regular programs of dynamic logic. The framework provides a simple formalization of the communicative actions in terms of their effects and preconditions and the specification of an interaction protocol by means of temporal constraints. We adopt a social approach to agent communication, where communication can be described in terms of changes in the social relations between participants, and protocols in terms of creation, manipulation and satisfaction of commitments among agents. The description of the interaction protocol and of communicative actions is given in a temporal action theory, and agent programs, when known, can be specified as complex actions (regular programs in DLTL). The paper addresses several kinds of verification problems (including the problem of verifying compliance of agents with the protocol), which can be formalized either as validity or as satisfiability problems in the temporal logic and can be solved by model checking techniques. In particular, we show that the verification of the compliance of an agent with the protocol requires to move to the logic DLTL^⊗, the product version of DLTL.