  In this paper, we present an approach for guaranteeing the completion of
complex tasks with cyber-physical systems (CPS). Specifically, we leverage
temporal logic trees constructed using Hamilton-Jacobi reachability analysis to
(1) check for the existence of control policies that complete a specified task
and (2) develop a computationally-efficient approach to synthesize the full set
of control inputs the CPS can implement in real-time to ensure the task is
completed. We show that, by checking the approximation directions of each state
set in the temporal logic tree, we can check if the temporal logic tree suffers
from the "leaking corner issue," where the intersection of reachable sets
yields an incorrect approximation. By ensuring a temporal logic tree has no
leaking corners, we know the temporal logic tree correctly verifies the
existence of control policies that satisfy the specified task. After confirming
the existence of control policies, we show that we can leverage the value
functions obtained through Hamilton-Jacobi reachability analysis to efficiently
compute the set of control inputs the CPS can implement throughout the
deployment time horizon to guarantee the completion of the specified task.
Finally, we use a newly released Python toolbox to evaluate the presented
approach on a simulated driving task.
