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

Abstract: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.

8 pages, 4 figures. Accepted for publication at the 65th IEEE Conference on Decision and Control (CDC 2026)

Robotics (cs.RO); Systems and Control (eess.SY)

arXiv:2604.12092 [cs.RO]

(or arXiv:2604.12092v2 [cs.RO] for this version)

https://doi.org/10.48550/arXiv.2604.12092 Focus to learn more arXiv-issued DOI via DataCite

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.