Guaranteed Completion of Complex Tasks via Temporal Logic Trees and Hamilton-Jacobi Reachability

TL;DR

This paper introduces a method combining temporal logic trees and Hamilton-Jacobi reachability to verify and synthesize control policies that guarantee complex task completion in cyber-physical systems, ensuring real-time implementation and correctness.

Contribution

It presents a novel approach that uses Hamilton-Jacobi reachability to construct and verify temporal logic trees, enabling guaranteed task completion with computational efficiency.

Findings

The approach can verify the existence of control policies for complex tasks.

It ensures the correctness of temporal logic trees by checking for leaking corners.

The method enables real-time synthesis of control inputs to guarantee task success.

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.