A Flexible Framework for Verifiable Agent Programming

There is an increasing number of agent-oriented programming languages that have working interpreters and platforms, with significant progress in the quality of such platforms over the last few years. With these platforms becoming more popular, and multi-agent systems being increasingly used for safety-critical applications, the need for verification techniques that apply to systems written in such languages is proportionally intensified. Building on our previous work on model checking for a particular agent-oriented programming language, we have developed a new approach whereby model checking techniques can be used directly on a variety of such languages. The approach also supports the verification of multi-agent systems where individual agents have been programmed in different agent languages.