@inproceedings{c4f0c3e7cf694fb79993fecc769e35fd,
title = "Enabling Behaviour Tree Verification via a Translation to BIP",
abstract = "A formal verification method for behavior tree (BT) is proposed. The method is based on a compositional model transformation of BT into the formal component-based system design framework BIP (Behavior-Interaction-Priority). The transformation encodes each BT node as an individual BIP component that is formally defined by an extended finite state automaton (FSA), and each BT edge as a set of interactions that describes the allowed coordination between components. The correctness proof of the model transformation is presented, and a prototype tool-chain has been implemented that enables the automated verification of BT. Two practical case studies show that the tool-chain can not only verify the correctness of BT, but also detect the potential design flaws automatically.",
keywords = "BIP framework, Behavior tree, Formal verification, Robotics",
author = "Qiang Wang and Huadong Dai and Yongxin Zhao and Min Zhang and Simon Bliudze",
note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.; 20th International Conference on Formal Aspects of Component Software, FACS 2024 ; Conference date: 09-09-2024 Through 10-09-2024",
year = "2024",
month = jan,
day = "1",
doi = "10.1007/978-3-031-71261-6\_1",
language = "English",
isbn = "9783031712609",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "3--20",
editor = "Diego Marmsoler and Meng Sun",
booktitle = "Formal Aspects of Component Software - 20th International Conference, FACS 2024, Proceedings",
}