A proof-system for the safe execution of tasks in multi-agent systems

Abstract

In this work, we propose an operational semantics based on a proof system for the consistent execution of tasks in a constrained multi-agent setting. The tasks represent services, and are associated with abstract specifications that express conditions on such services. The constraints, contained in the body of the agents, may include - but are not limited to - policies on provided services, and limitations about the use and allocation of bounded resources. The contribution of this work is twofold. Firstly, a formalism and an operational semantics is introduced, to express the way agents can coordinate their requests of services, and to verify that they do not collide with each other's conditions. Then, we prove the soundness and completeness of such operational semantics to be used to verify the correct execution of tasks. © 2002 Springer-Verlag.