Verifying Communicating Agents by Model Checking in a Temporal Action Logic


Laura Giordano, Alberto Martelli, Camilla Schwind

Logics in Artificial Intelligence, pages 57-69
LNCS 3229,  2004
Springer
Jóse Júlio Alferes, João Leite (eds.)

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.

 @inproceedings{verifyingdltl-lncs3229,
Author = {Giordano, Laura and Martelli, Alberto and Schwind, Camilla},
Booktitle = {Logics in Artificial Intelligence},
Doi = {10.1007/978-3-540-30227-8_8},
Editor = {Alferes, J{\'o}se J{\'u}lio and Leite, Jo{\~a}o},
Isbn = {978-3-540-23242-1},
Pages = {57--69},
Publisher = {Springer},
Series = {LNCS},
Title = {Verifying Communicating Agents by Model Checking in a Temporal Action Logic},
Url = {http://rd.springer.com/chapter/10.1007/978-3-540-30227-8_8},
Volume = 3229,
Year = 2004

Tags:

Publication

— authors

Laura Giordano, Alberto Martelli, Camilla Schwind

— editors

Jóse Júlio Alferes, João Leite

— status

published

— sort

paper in proceedings

Venue

— volume

Logics in Artificial Intelligence

— series

LNCS

— volume

3229

— pages

57-69

— publication date

2004

URLs

original page

Identifiers

— DOI

10.1007/978-3-540-30227-8_8

— print ISBN

978-3-540-23242-1

BibTeX

— BibTeX ID
verifyingdltl-lncs3229
— BibTeX category
inproceedings

Partita IVA: 01131710376 - Copyright © 2008-2022 APICe@DISI Research Group - PRIVACY