Verifying Safety of Behaviour Trees in Event-B

• URL: http://arxiv.org/abs/2209.14045v1
• Date: Wed, 28 Sep 2022 12:26:50 GMT
• Title: Verifying Safety of Behaviour Trees in Event-B
• Authors: Matteo Tadiello (KTH), Elena Troubitsyna (KTH)
• Abstract summary: Behavior Trees (BT) are becoming increasingly popular in the robotics community. We propose a formal specification of Behavior Trees and a methodology to prove invariants of already used trees.
• Score: 0.0
• License: http://creativecommons.org/publicdomain/zero/1.0/
• Abstract: 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.

Related papers

• Execution Semantics of Behavior Trees in Robotic Applications [0.6718184400443239]
  This document aims at describing, in a suitably precise and though informal way, the execution semantics of Behavior Trees as used in Robotics applications, with particular attention to the Halt semantics.
  arXiv  Detail & Related papers  (2024-07-31T18:08:59Z)
• Integrating Intent Understanding and Optimal Behavior Planning for Behavior Tree Generation from Human Instructions [5.31484618181979]
  Behavior Tree (BT) is an appropriate control architecture for robots executing tasks following human instructions. This paper proposes a two-stage framework for BT generation, which first employs large language models to interpret goals from high-level instructions. We represent goals as well-formed formulas in first-order logic, effectively bridging intent understanding and optimal behavior planning.
  arXiv  Detail & Related papers  (2024-05-13T05:23:48Z)
• Learning a Decision Tree Algorithm with Transformers [75.96920867382859]
  We introduce MetaTree, a transformer-based model trained via meta-learning to directly produce strong decision trees. We fit both greedy decision trees and globally optimized decision trees on a large number of datasets, and train MetaTree to produce only the trees that achieve strong generalization performance.
  arXiv  Detail & Related papers  (2024-02-06T07:40:53Z)
• Tree Prompting: Efficient Task Adaptation without Fine-Tuning [112.71020326388029]
  Tree Prompting builds a decision tree of prompts, linking multiple LM calls together to solve a task. Experiments on classification datasets show that Tree Prompting improves accuracy over competing methods and is competitive with fine-tuning.
  arXiv  Detail & Related papers  (2023-10-21T15:18:22Z)
• An Extended Convergence Result for Behaviour Tree Controllers [0.0]
  Behavior trees (BTs) are an optimally modular framework to assemble hierarchical hybrid control policies. We study the convergence of BTs, in the sense of reaching a desired part of the state space.
  arXiv  Detail & Related papers  (2023-08-17T14:05:45Z)
• Robot Behavior-Tree-Based Task Generation with Large Language Models [14.384843227828775]
  We propose a novel behavior-tree-based task generation approach that utilizes state-of-the-art large language models. We propose a Phase-Step prompt design that enables a hierarchical-structured robot task generation and further integrate it with behavior-tree-embedding-based search to set up the appropriate prompt. Our behavior-tree-based task generation approach does not require a set of pre-defined primitive tasks.
  arXiv  Detail & Related papers  (2023-02-24T22:53:10Z)
• RLET: A Reinforcement Learning Based Approach for Explainable QA with Entailment Trees [47.745218107037786]
  We propose RLET, a Reinforcement Learning based Entailment Tree generation framework. RLET iteratively performs single step reasoning with sentence selection and deduction generation modules. Experiments on three settings of the EntailmentBank dataset demonstrate the strength of using RL framework.
  arXiv  Detail & Related papers  (2022-10-31T06:45:05Z)
• Social Interpretable Tree for Pedestrian Trajectory Prediction [75.81745697967608]
  We propose a tree-based method, termed as Social Interpretable Tree (SIT), to address this multi-modal prediction task. A path in the tree from the root to leaf represents an individual possible future trajectory. Despite the hand-crafted tree, the experimental results on ETH-UCY and Stanford Drone datasets demonstrate that our method is capable of matching or exceeding the performance of state-of-the-art methods.
  arXiv  Detail & Related papers  (2022-05-26T12:18:44Z)
• Learning Behavior Trees with Genetic Programming in Unpredictable Environments [7.839247285151348]
  We show that genetic programming can be effectively used to learn the structure of a behavior tree. We demonstrate that the learned BTs can solve the same task in a realistic simulator, reaching convergence without the need for task specifics.
  arXiv  Detail & Related papers  (2020-11-06T09:28:23Z)
• MurTree: Optimal Classification Trees via Dynamic Programming and Search [61.817059565926336]
  We present a novel algorithm for learning optimal classification trees based on dynamic programming and search. Our approach uses only a fraction of the time required by the state-of-the-art and can handle datasets with tens of thousands of instances.
  arXiv  Detail & Related papers  (2020-07-24T17:06:55Z)
• Parameterizing Branch-and-Bound Search Trees to Learn Branching Policies [76.83991682238666]
  Branch and Bound (B&B) is the exact tree search method typically used to solve Mixed-Integer Linear Programming problems (MILPs) We propose a novel imitation learning framework, and introduce new input features and architectures to represent branching.
  arXiv  Detail & Related papers  (2020-02-12T17:43:23Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.