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.

翻译：本文提出了一种确保信息物理系统（CPS）完成复杂任务的方法。具体而言，我们利用通过Hamilton-Jacobi可达性分析构建的时序逻辑树：（1）检验是否存在能够完成指定任务的控制策略；（2）开发一种计算高效的方法，以综合CPS可实时实现的全部控制输入集合，从而确保任务完成。我们证明：通过检查时序逻辑树中每个状态集的逼近方向，可判定该树是否存在"泄漏角问题"——即可达集交集导致错误逼近的情况。确保时序逻辑树无泄漏角后，即可确认该树能正确验证满足指定任务的控制策略的存在性。在确认控制策略存在后，我们进一步证明可利用Hamilton-Jacobi可达性分析获得的价值函数，高效计算CPS在整个部署时间跨度内可执行的控制输入集合，从而保证指定任务的完成。最后，使用新发布的Python工具箱在模拟驾驶任务上评估了所提方法。