Ternary Logic Encodings of Temporal Behavior Trees with Application to Control Synthesis

1. Problem Statement

Autonomous systems require robust methods for task modeling and control synthesis. While Signal Temporal Logic (STL) offers rich expressivity for specifying spatiotemporal behaviors, it struggles with long-horizon planning and complex fallback mechanisms (e.g., "if task A fails, try B"). Behavior Trees (BTs) provide an intuitive, modular graphical interface for such hierarchical strategies but lack rigorous formal models for correct-by-construction control synthesis.

Existing approaches to formalizing BTs (Temporal Behavior Trees or TBTs) rely on offline post-hoc analysis or trace repair using Boolean logic. These methods fail to capture the dynamic nature of BT execution, specifically the "Running" state, where a task is neither fully satisfied nor failed. Furthermore, standard STL encodings for control synthesis often assume infinite trajectories or require the entire horizon to be known, making them unsuitable for partial trajectory analysis or systems with uncertainty.

The Core Challenge: How to formally encode Behavior Trees and their temporal operators into a mathematical framework suitable for mixed-integer optimization (control synthesis) that accounts for:

1. The three-state logic of BTs (Success, Failure, Running).
2. Partial trajectories where the future is unknown.
3. System uncertainty (measurements that are neither clearly true nor false).

2. Methodology

The authors propose a framework that reformulates TBTs using Kleene's Strong Logic ($K_3$), a ternary logic system, and encodes these semantics into Mixed-Integer Linear Programming (MILP) constraints.

A. Ternary Logic Foundation ($K_3$)

Instead of standard Boolean logic (True/False), the authors introduce a third value, Unknown ($U$), to represent the "Running" state of a BT node or indeterminate system measurements.

• Truth Values: $\{F, U, T\}$ corresponding to $\{-1, 0, +1\}$.
• Logic Operations: Defined via Kleene algebra tables (e.g., $T \land U = U$, $F \lor U = U$).
• Significance: This allows the system to handle cases where a trajectory has not yet satisfied or violated a specification, enabling reasoning over partial trajectories.

B. Ternary Signal Temporal Logic (STL)

The authors extend STL semantics to operate over $K_3$ and partial trajectories (finite time horizons $t_2$).

• Signal Predicates: Defined with an uncertainty threshold $\delta$. If $f(x_t) \ge \delta$, the value is $T$; if $f(x_t) \le -\delta$, it is $F$; if $-\delta < f(x_t) < \delta$, it is $U$.
• Temporal Operators: The "Always" ($\square$) and "Eventually" ($\diamond$) operators are redefined to handle the relationship between the search window (the time interval required by the operator) and the partial horizon (the current known trajectory length).
  • If the search window is fully within the horizon, standard logic applies.
  • If the window exceeds the horizon, the result is $U$ (Unknown) unless a "short-circuit" occurs (e.g., a conjunction encounters a $F$ immediately, making the whole expression $F$ regardless of the unknown future).

C. Mixed-Integer Encodings

The paper develops specific encodings to translate these ternary logic rules into constraints for a Mixed-Integer Quadratic Program (MIQP).

• Decision Variables: Ternary integers $z \in \{-1, 0, +1\}$ representing the satisfaction of a formula at a specific time step.
• Encoding Strategy:
  • Predicates: Encoded using binary variables to enforce the affine constraints on the state $x_t$ relative to $\delta$.
  • Logical Connectives: Min/Max operations are used to encode $\land$ (min) and $\lor$ (max) over the ternary set.
  • TBT Operators (Seq/Sel):
    • Sequence ($\rightarrow$): Requires sub-formulas to be satisfied sequentially. The encoding searches for a split point $\tau$ where the first part satisfies $\phi_1$ and the remainder satisfies $\phi_2$.
    • Selector ($?$): Requires at least one sub-formula to be satisfied. The encoding searches for a split point where either the first part satisfies $\phi_1$ OR the remainder satisfies $\phi_2$.
• Complexity: The authors note that while standard STL encodings are linear in time complexity $O(T)$, TBT encodings involving $k$ sub-formulas scale as $O(T^{k+1})$ due to the nested search over time splits.

D. Control Synthesis Problem

The framework formulates an optimal control problem for linear discrete-time systems:
$$\min \sum u_t^T R u_t$$
Subject to:

• System dynamics ($x_{t+1} = Ax_t + Bu_t$).
• Input constraints.
• TBT Satisfaction Constraint: The synthesized trajectory must satisfy the TBT formula $\phi$ starting at time $t^*$.

3. Key Contributions

1. Formalization of BTs in $K_3$: The paper concretizes the formalization of Behavior Trees using ternary logic, explicitly mapping the "Running" state to the "Unknown" truth value.
2. Ternary STL Semantics: It defines the qualitative semantics of STL over partial trajectories using $K_3$, allowing formulas to be evaluated even when the full horizon is not yet known or when measurements are uncertain.
3. Mixed-Integer Encodings: The authors provide the first mixed-integer linear encodings for TBT operators (Sequence and Selector) over ternary logic, enabling correct-by-construction control synthesis.
4. Demonstration of Utility: The framework is validated through two case studies solving optimal control problems for linear dynamical systems, proving that TBTs can generate feasible, optimal trajectories that handle complex fallback logic.

4. Results and Case Studies

The authors validated the framework using the Gurobi solver on two scenarios:

• Case Study 1: Discrete-Time Double Integrator (Mobile Robot)

  • Task: Navigate to Goal A, then check battery. If $\ge 80\%$, go to Goal B; else, go to Goal C (charger) then Goal B.
  • Outcome: The solver successfully synthesized trajectories for two different initial battery states.
    • High Battery: Robot went A $\to$ B.
    • Low Battery: Robot went A $\to$ C $\to$ B.
  • Performance: Solved to global optimality in ~97 seconds for a 25-step horizon.

• Case Study 2: Multi-Agent Planning

  • Task: Three agents must sequentially reach specific goals while avoiding obstacles and maintaining a minimum separation distance.
  • Outcome: The system synthesized trajectories where agents naturally queued to pass through narrow obstacle corridors to satisfy the safety constraints.
  • Performance: Solved for 3 agents over a 20-step horizon in ~307 seconds.

5. Significance and Impact

• Bridging the Gap: This work bridges the gap between the intuitive design of Behavior Trees and the rigorous requirements of formal control synthesis. It moves BTs from being purely simulation-based or post-hoc verified tools to being synthesis-ready specifications.
• Handling Uncertainty: By using ternary logic, the framework naturally handles sensor uncertainty and partial execution states, which are critical for real-world autonomous systems but often ignored in Boolean-based synthesis.
• Correct-by-Construction: The approach guarantees that the generated control policies satisfy safety and behavioral requirements by construction, rather than relying on trial-and-error or reinforcement learning which may not guarantee safety.
• Future Directions: The authors note that while the current complexity is high for deep trees, the method opens the door for applying these techniques to nonlinear systems and more complex hierarchical planning problems.

In summary, the paper presents a mathematically rigorous method to translate high-level, modular behavior tree specifications into optimization problems, enabling autonomous systems to generate optimal, safe, and robust control strategies that adapt to failures and uncertainties.