Model Checking is a powerful automated proof technique based on temporal logics. Model checking has been applied in many different domains. However, there has been relatively little work on the application of model checking to multi-agent systems (MAS). The primary reason for this appears to be that MAS specifications are usually considered too large for model checking.
Around a year ago I gave an SSP talk outlining the benefits of applying model checking to MAS. However, I also outlined a number of problems with the naive approach. In this talk I will outline the ongoing developments in model checking of MAS as part of the SLIE grant, and our proposed solution to a number of these problems.
Note: Attendance of my previous model checking talk is NOT a prerequisite of this talk!