CAN-Verify: Automated analysis for BDI agents

We present CAN-Verify , an automated tool for analysing BDI agents written in the Conceptual Agent Notation ( Can ) language. CAN-Verify includes support for syntactic error detection before agent execution, agent program interpretation (running agents), and model-checking of agent programs (analysing agents). The model checking supports verifying the correctness of agents against both generic agent requirements, such as if a task is accomplished, and user-defined requirements, such as certain beliefs eventually holding. The latter can be expressed in structured natural language, allowing the tool to be used by agent programmers without formal training in the underlying verification techniques.