Abstract:
Specification and verification of multi-agent programs is a key problem in agent research and development. One may for example be interested in checking if a specific subset of individual agent programs can achieve a particular state of their shared environment, or if they can protect the system from entering a ``bad'' state. This paper focuses on BDI-based multi-agent programs that consist of a finite set of BDI-based agent programs executed concurrently. We choose alternating-time temporal logic (ATL) for expressing such properties. However, the original ATL is based on a synchronous model of multi-agent computation while most (if not all) multi-agent programming frameworks use asynchronous semantics where activities of different agents are interleaved. Moreover, unlike in ATL, our agent programs do not have perfect information about the current global state of the system. They are not appropriate subjects of modal epistemic logic either (since they do not know the global model of the system). This paper presents our first attempt at adapting the semantics of ATL to reasoning about asynchronous multi-agent programs.

Individual and Collective Reasoning Group @ University of Luxembourg
Computational Intelligence Group @ Clausthal University of Technology	Last modified 2010-01-08