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

TL;DR

This paper introduces a ternary logic-based formalism for Temporal Behavior Trees, enabling control synthesis and verification for linear systems through mixed-integer optimization.

Contribution

It reformulates TBTs using ternary-valued STL, allowing for correct-by-construction control strategies and offline analysis within a unified framework.

Findings

Successfully encodes partial trajectories and TBTs using mixed-integer linear constraints.

Enables control synthesis for linear dynamical systems via mixed-integer optimization.

Demonstrates effectiveness by solving optimal control problems.

Abstract

Behavior Trees (BTs) provide designers 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 for control synthesis. Ternary logic introduces a third truth value \textit{Unknown}, formally capturing cases where a trajectory has neither fully satisfied or dissatisfied 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.