Model checking multiagent systems

We model agents as processes able to have Beliefs, desires, and Intentions (BDI agents). In this talk we briefly describe an algorithm which allows us to validate, via model checking, BDI agents. The focus is on the underlying ideas and theory. The crucial technical step solves the problem of how to model check BDI attitudes. In fact, BDI attitudes can be nested at any level, and, for any level of nesting, we have an infinite number of them.