Synthesis of correct-by-construction behavior trees

Michele Colledanchise; Richard M. Murray; Petter Ögren

IROS 2017poster53 citations

Synthesis of correct-by-construction behavior trees

Michele Colledanchise, Richard M. Murray, Petter Ögren

Abstract

In this paper we study the problem of synthesizing correct-by-construction Behavior Trees (BTs) controlling agents in adversarial environments. The proposed approach combines the modularity and reactivity of BTs with the formal guarantees of Linear Temporal Logic (LTL) methods. Given a set of admissible environment specifications, an agent model in form of a Finite Transition System and the desired task in form of an LTL formula, we synthesize a BT in polynomial time, that is guaranteed to correctly execute the desired task. To illustrate the approach, we present three examples of increasing complexity.

BibTeX

@inproceedings{iros2017_synthesisofcorre,
  title = {Synthesis of correct-by-construction behavior trees},
  author = {Michele Colledanchise and Richard M. Murray and Petter Ögren},
  booktitle = {IROS 2017},
  year = {2017}
}