Search papers, labs, and topics across Lattice.
This paper reformulates Temporal Behavior Trees (TBTs) using a ternary-valued Signal Temporal Logic (STL) to enable control synthesis, addressing the limitations of existing offline analysis methods. The ternary logic introduces an "Unknown" truth value to handle partial satisfaction of specifications. Mixed-integer linear encodings are then developed for both STL and TBTs under this ternary logic, enabling correct-by-construction control strategies for linear dynamical systems via mixed-integer optimization.
Achieve correct-by-construction control for autonomous systems by encoding Temporal Behavior Trees with ternary logic, allowing for reasoning about partial satisfaction of temporal specifications.
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.
