Reasoning about strategies of multi-agent programs

Abstract

Verification of multi-agent programs is a key problem in agent research and development. This paper focuses on 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 properties of such programs. 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 for modal epistemic logic either (since they do not know the global model of the system). We begin by adapting the semantics of ATL to the situation at hand; then, we consider the verification problem in the new setting and present some preliminary results. Copyright © 2010, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.