Welcome to the MoVe4BT tool website! MoVe4BT is a specialized tool for the formal modeling and verification of Behavior Trees (BTs). It uses the Timed CSPbt modeling language, which extends Timed CSP with composition operators and basic processes. The tool is implemented based on the Process Analysis Toolkit (PAT) and the Groot graphical editor, providing a user-friendly interface that allows users to easily construct BTs graphically and specify Linear Temporal Logic (LTL) properties as well as timed properties.

Key features of MoVe4BT include:

Graphical Editing: With an intuitive drag-and-drop interface, users can easily create and edit BT structures without writing any code or dealing with the underlying formal modeling language.

Model Verification: Utilizing model checking techniques, MoVe4BT can verify whether a BT satisfies the specified properties and generates detailed counterexamples when the model does not meet the properties, helping users identify and fix errors.

Comprehensive Documentation: The website offers extensive user manuals and tutorials to help new users get started quickly and guide advanced users through complex verification tasks.

Whether you are a novice or an experienced developer, MoVe4BT can help you streamline the modeling and verification process of BTs, improve work efficiency, and ensure the reliability and safety of your system. Download and experience MoVe4BT today to explore the possibilities of automated verification!

• Introduction

• Manual

• Tutorial

• Case Study

• Supplemental Material

Contacts

Please feel free to contact us if you have any questions about MoVe4BT.

• Peishan Huang (huang_ps@nudt.edu.cn)
• Weijiang Hong (hongweijiang17@nudt.edu.cn)
• Zhenbang Chen (zbchen@nudt.edu.cn)
• Ji Wang (wj@nudt.edu.cn)