EffBT: An Efficient Behavior Tree Reactive Synthesis and Execution Framework
Formal Methods
Behavior Trees (BTs), originated from the control of Non-Player-Characters (NPCs), have been widely embraced in robotics and software engineering communities due to their modularity, reactivity, and other beneficial characteristics. It is highly desirable to synthesize BTs automatically. The consequent challenges are to ensure the generated BTs semantically correct, well-structured, and efficiently executable. To address these challenges, in this paper, we present a novel reactive synthesis method for BTs, namely EffBT, to generate correct and efficient controllers from formal specifications in GR(1) automatically. The idea is to construct BTs soundly from the intermediate strategies derived during the algorithm of GR(1) realizability check. Additionally, we introduce pruning strategies and use of \textit{Parallel} nodes to improve BT execution, while none of the priors explored before. We prove the soundness of the EffBT method, and experimental results across various scenarios and datasets demonstrate its effectiveness.
Wed 30 AprDisplayed time zone: Eastern Time (US & Canada) change
11:00 - 12:30 | Formal Methods 1Research Track / New Ideas and Emerging Results (NIER) at 103 Chair(s): Cristian Cadar Imperial College London | ||
11:00 15mTalk | SpecGen: Automated Generation of Formal Program Specifications via Large Language ModelsFormal Methods Research Track Lezhi Ma Nanjing University, Shangqing Liu Nanyang Technological University, Yi Li Nanyang Technological University, Xiaofei Xie Singapore Management University, Lei Bu Nanjing University | ||
11:15 15mTalk | Gpass: a Goal-adaptive Neural Theorem Prover based on Coq for Automated Formal VerificationFormal Methods Research Track Yizhou Chen Peking University, Zeyu Sun Institute of Software, Chinese Academy of Sciences, Guoqing Wang Peking University, Dan Hao Peking University | ||
11:30 15mTalk | AI-Assisted Autoformalization of Combinatorics Problems in Proof AssistantsFormal Methods New Ideas and Emerging Results (NIER) | ||
11:45 15mTalk | Formally Verified Binary-level Pointer AnalysisFormal Methods Research Track Freek Verbeek Open Universiteit & Virginia Tech, Ali Shokri Virginia Tech, Daniel Engel Open University Of The Netherlands, Binoy Ravindran Virginia Tech | ||
12:00 15mTalk | EffBT: An Efficient Behavior Tree Reactive Synthesis and Execution FrameworkFormal Methods Research Track ziji wu National University of Defense Technology, yu huang National University of Defense Technology, peishan huang National University of Defense Technology, shanghua wen National University of Defense Technology, minglong li National University of Defense Technology, Ji Wang National University of Defense Technology | ||
12:15 7mTalk | SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code GenerationFormal Methods New Ideas and Emerging Results (NIER) Junjie Sheng East China Normal University, Yanqiu Lin East China Normal University, Jiehao Wu East China Normal University, Yanhong Huang East China Normal University, Jianqi Shi East China Normal University, Min Zhang East China Normal University, Xiangfeng Wang East China Normal University | ||
12:22 7mTalk | Listening to the Firehose: Sonifying Z3’s Behavior New Ideas and Emerging Results (NIER) | ||