]> 2026-04-15T01:56:27+00:00 Synthesis of Correct-by-Construction Behavior Trees 0 en 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. Michele Colledanchise Richard M. Murray and Petter Ogren 2017e Submitted, 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) cmo17-iros Conference paper 2017-07-23T17:16:30Z 2457958.2197917 Synthesis of Correct-by-Construction Behavior Trees Title 102 en Title