Temporal logics have garnered significant attention in the control community due to their use for formal control synthesis, namely for the synthesis of control policies with provable correctness guarantees for more complex and interesting properties than traditional control objectives. Formal control under temporal logics is fundamentally challenging though, particularly when dealing with uncertain infinite systems and complex temporal logic specifications for real-time task planing, as the established methods struggle with handling models in high dimensions and with accommodating online deployment. In this article, we propose Temporal Logic Trees (TLT) as a mitigation for these challenges. TLT are constructed from Linear Temporal Logic (LTL) formulae via reachability analysis, offering an abstraction-free design method. Building upon the TLT framework, we present approaches for adaptive task planning and formal control synthesis that are usable on both finite and infinite systems. Furthermore, we demonstrate the applicability of our approach for online control synthesis, particularly in addressing time-varying tasks: namely, our method allows for dynamic online updates of the specifications, which showcases its practical utility and flexibility.
