Abstract
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.
Abstract (translated)
在本文中，我们提出了一种使用哈密顿-雅可比到达性分析构建的时间逻辑树来保证具有复杂任务的 cyber-physical系统（CPS）完成任务的方法。具体来说，我们利用哈密顿-雅可比到达性分析构建的时间逻辑树来（1）检查是否存在完成指定任务的控制策略，（2）开发一种计算高效的方法来合成CPS在实时过程中可以实现的所有控制输入，以确保任务完成。我们证明了，通过检查时间逻辑树中每个状态集中的近似方向，我们可以检查时间逻辑树是否受到“泄漏角落问题”的影响，即可到达集的交集给出错误的近似。通过确保时间逻辑树没有泄漏角落，我们知道时间逻辑树正确验证了满足指定任务的控制策略的存在。在确认控制策略的存在后，我们证明了我们可以利用哈密顿-雅可比到达性分析获得的值函数来有效地计算CPS在部署时间视野内可以实现的所有控制输入，以确保完成指定任务。最后，我们使用一个新的Python工具箱评估了所提出的方法在模拟驾驶任务上的效果。
URL
https://arxiv.org/abs/2404.08334
