  This paper studies the robust satisfiability check and online control
synthesis problems for uncertain discrete-time systems subject to signal
temporal logic (STL) specifications. Different from existing techniques, this
work proposes an approach based on STL, reachability analysis, and temporal
logic trees. Firstly, a real-time version of STL semantics and a tube-based
temporal logic tree are proposed. We show that such a tree can be constructed
from every STL formula. Secondly, using the tube-based temporal logic tree, a
sufficient condition is obtained for the robust satisfiability check of the
uncertain system. When the underlying system is deterministic, a necessary and
sufficient condition for satisfiability is obtained. Thirdly, an online control
synthesis algorithm is designed. It is shown that when the STL formula is
robustly satisfiable and the initial state of the system belongs to the initial
root node of the tube-based temporal logic tree, it is guaranteed that the
trajectory generated by the controller satisfies the STL formula. The
effectiveness of the proposed approach is verified by an automated car
overtaking example.
