|Home||Online Resources||Table of Contents|
Journal of Logic and Computation, Volume 8, Issue 3: June 1998.
Tableau methods for formal verification of multi-agent distributed systems
Dipartimento di Informatica e Sistemistica, Universita di Roma 'La Sapienza', via Salaria 113, I-00198 Roma, Italy, E-mail: email@example.com
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-modal 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.