@inproceedings{5ccf290dd87b4e7bb85fa81450735f2d,
title = "Verifying communicating agents by model checking in a temporal action logic",
abstract = "In this paper we address the problem of specifying and verifying systems of communicating agents in a Dynamic Linear Time Temporal Logic (DLTL). This logic provides a simple formalization of the communicative actions in terms of their effects and preconditions. Furthermore it allows to specify interaction protocols by means of temporal constraints representing permissions and commitments. Agent programs, when known, can be formulated in DLTL as complex actions (regular programs). The paper addresses several kinds of verification problems including the problem of compliance of agents to the protocol, and describes how they can be solved by model checking in DLTL using automata.",
author = "Laura Giordano and Alberto Martelli and Camilla Schwind",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2004.; 9th European Conference on Logics in Artificial Intelligence, JELIA 2004 ; Conference date: 27-09-2004 Through 30-09-2004",
year = "2004",
doi = "10.1007/978-3-540-30227-8\_8",
language = "English",
isbn = "3540232427",
series = "Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)",
publisher = "Springer Verlag",
pages = "57--69",
editor = "Alferes, \{Jose Julio\} and Joao Leite",
booktitle = "Logics in Artificial Intelligence - 9th European Conference, JELIA 2004",
address = "Germany",
}