CAN-verify: A Verification Tool For BDI Agents

CAN-verify is an automated tool that aids the development, verification, and analysis of BDI agents written in the Conceptual Agent Notation (Can) language. It does not require users to be familiar with verification techniques. CAN-verify supports syntactic error checking, interpretation of programs (running agents), and exhaustive exploration of all possible executions (agent verification and analysis) to check against both generic agent requirements, such as if a task can be achieved successfully, and user-defined requirements, such as whether a certain belief eventually holds. Simple examples of Unmanned Aerial Vehicles (UAV) and autonomous patrol robots illustrate the tool in action.