Skip Navigation

Journal of Logic and Computation 1998 8(3):373-400; doi:10.1093/logcom/8.3.373
© 1998 by Oxford University Press
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by MASSACCI, F.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

Original Articles

Tableau Methods for Formal Verification of Multi-Agent Distributed Systems

FABIO MASSACCI

Dipartimento di Information e Sistemistica Universitá di Roma "La Sapienza", via Salaria 113, 1-00198 Roma, Italy. E-mail: massacci{at}dis.uniromal.it

Formal verification is a key step in the development of trusted and reliable multi-agent distributed systems. This is particularly relevant when security concerns such as privacy, integrity and availability impose limitations on the operations that can be performed on sensitive data. The aim of access control is to limit what agents (humans, programs, softbots, etc.) of distributed systems can do directly or indirectly by delegating their powers and tasks. As the size of the systems and the sensitivity of data increase, the availability of automated reasoning methods becomes essential for logical analysis of access control.

This paper presents a prefixed tableau method for the calculus of access control developed at the Digital System Research Center. This calculus is particularly interesting for a number of reasons. First it was the basis for the development and the verification of an implemented system. Second, it poses many technical challenges for classical modal tableaux: it lacks the tree-model property, has some features of the universal modality, and can introduce delegation certificates between agents "on-the-fly" not compilable into axiom schemata.

Keywords: Prefixed tableaux; access control; DEC-SRC calculus; multi-agent distributed systems; modal logic


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer: Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.