Behavior Trees (BTs) provide designers with an intuitive graphical interface to construct long-horizon plans for autonomous systems. To ensure their correctness and safety, rigorous formal models and verification techniques are essential. Temporal BTs (TBTs) offer a promising approach by leveraging existing temporal logic formalisms to specify and verify the executions of BTs. However, this analysis is currently limited to offline post hoc analysis and trace repair. In this paper, we reformulate TBTs using a ternary-valued Signal Temporal Logic (STL) amenable to control synthesis. Ternary logic introduces a third truth value Unknown, formally capturing cases where a trajectory has neither fully satisfied nor violated a specification. We propose mixed-integer linear encodings for partial trajectory STL and TBTs over ternary logic, allowing for correct-by-construction control strategies for linear dynamical systems via mixed-integer optimization. We demonstrate the utility of our framework by solving optimal control problems.
Figures & tables
Fig. 1: Example BT for a mobile robot task. BTs are read from left to right with the colored nodes representing the BT control operators and the leaf nodes representing execution nodes. This BT specifies that the mobile robot must first navigate to goal A . Then, if the battery is greater than or equal to 80% , proceed to goal B . Otherwise, if the battery is less than 80% , navigate to goal C then proceed to goal B .
Fig. 2: Synthesized Robot Trajectories satisfying the TBT formula ( 10 ) for two different initial battery levels. When the battery level is below 80% , the robot must return to the charger (location C ) before proceeding to location B . In both cases the robot starts at the center of location C and is initially at rest.
Fig. 3: Synthesized trajectories for three agents satisfying the TBT formula ( 11 ) with maximum finite horizon N=20 time steps and time interval δt=0.5 s. Sub-level formula φ1 specifies that eventually agent 1 ( blue ) shall reach goal C , agent 2 ( red ) shall reach goal A , and agent 3 ( green ) shall reach goal B . Sub-level formula φ2 specifies that eventually agent 1 shall reach goal B , agent 2 shall reach goal C , and agent 3 shall reach goal A . The model has 354 continuous variables, 2040 integer variables, 2040 linear constraints, and 114 quadratic objective terms. The model was solved to global optimality in 307.75 seconds on an Ubuntu 22.04 machine with an AMD Ryzen 9 7950X 16 Core CPU and 128GB of memory.
Fig. 4: The synthesized multi-agent trajectories elicit a queuing phenomenon when passing through the obstacles.