Verifying Safety of Behaviour Trees in Event-B
Behavior Trees (BT) are becoming increasingly popular in the robotics community. The BT tool is well suited for decision-making applications allowing a robot to perform complex behavior while being explainable to humans as well. Verifying that BTs used are well constructed with respect to safety and reliability requirements is essential, especially for robots operating in critical environments. In this work, we propose a formal specification of Behavior Trees and a methodology to prove invariants of already used trees, while keeping the complexity of the formalization of the tree simple for the final user. Allowing the possibility to test the particular instance of the behavior tree without the necessity to know the more abstract levels of the formalization.
Code (0)
등록된 구현이 없습니다.
Tasks
Decision MakingMethods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Verifying And Interpreting Neural Networks using Finite Automata
Verifying properties and interpreting the behaviour of deep neural networks (DNN) is an important task given their ubiquitous use in applications, including safety-critical ones, and their black-box nature. We propose an…
Adversarial RobustnessSafety Verification of Neural Network Controlled Systems
In this paper, we propose a system-level approach for verifying the safety of neural network controlled systems, combining a continuous-time physical system with a discrete-time neural network based controller. We assume…
Safety Verification of Decision-Tree Policies in Continuous Time
Decision trees have gained popularity as interpretable surrogate models for learning-based control policies. However, providing safety guarantees for systems controlled by decision trees is an open challenge. We show tha…
Learning Invariants using Decision Trees
The problem of inferring an inductive invariant for verifying program safety can be formulated in terms of binary classification. This is a standard problem in machine learning: given a sample of good and bad points, one…
Binary ClassificationImproving the Modularity of AUV Control Systems using Behaviour Trees
In this paper, we show how behaviour trees (BTs) can be used to design modular, versatile, and robust control architectures for mission-critical systems. In particular, we show this in the context of autonomous underwate…