@inproceedings{f7a343ebf0e04029b13cbeee486c5a64,
title = "Specifying and verifying systems of communicating agents in a temporal action logic",
abstract = "In this paper we develop a logical framework for specifying and verifying systems of communicating agents. The framework is based on a Dynamic Linear Time Temporal Logic (DLTL). It 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 (as proposed by Singh): 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 compliance of agents to 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.",
author = "Laura Giordano and Alberto Martelli and Camilla Schwind",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2003.; 8th Congress of the Italian Association for Artificial Intelligence ; Conference date: 23-09-2003 Through 26-09-2003",
year = "2003",
doi = "10.1007/978-3-540-39853-0_22",
language = "English",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "262--274",
editor = "Amedeo Cappelli and Franco Turini",
booktitle = "AI*IA 2003",
address = "Germany",
}