Reasoning about strategies of multi-agent programs

10 years 28 days ago
Reasoning about strategies of multi-agent programs
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. Categories and Subject Descriptors I.2.5 [Artificial Int...
Mehdi Dastani, Wojciech Jamroga
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where ATAL
Authors Mehdi Dastani, Wojciech Jamroga
Comments (0)