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

TL;DR

This work addresses guaranteeing completion of complex tasks for cyber-physical systems by integrating temporal logic trees (TLTs) with Hamilton-Jacobi reachability. It first constructs a TLT from HJ reachability to check the existence of control policies that satisfy a finite-horizon LTL specification, then computes least-restrictive real-time control input sets from the HJ value functions to guarantee task completion. Key contributions include a formal algorithm for ctrlExists to detect leaking corners, and a computationally efficient method to synthesize explicit control sets from TLTs, demonstrated on a nonlinear 5-state bicycle driving task with the open-source pyspect toolbox. The results show that the combination of TLT feasibility analysis and HJ-based control synthesis yields rigorous guarantees and practical, real-time control constraints, enabling robust task completion under changes like blocked paths. The work also provides a practical software pathway through pyspect for researchers and practitioners to apply these guarantees to CPS tasks.

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.

Figures (4)

• Figure 1: We illustrate and annotate an example temporal logic tree that is used to guarantee the completion of a vehicle parking task.
• Figure 2: We illustrate and describe all the different branches that can occur in a TLT and their corresponding state set and operator nodes.
• Figure 3: The full, under-approximating satisfaction set for the parking task computed by constructing the temporal logic tree using HJ reachability analysis
• Figure 4: We illustrate the deployment of the simulated vehicle for the specified parking task. In the two larger plots, we show the full environment and an xy projection of the 5D satisfaction state set of the constructed TLT. In the smaller plots, we show the velocity-heading projection of the constructed TLT's satisfaction set (in blue) and the computed least-restrictive control set (in green) for different states and times throughout the task completion.

Theorems & Definitions (26)

• Definition II.1
• Definition II.2
• Definition II.3
• Definition II.4
• Definition II.5
• Definition II.6
• Definition IV.1
• Lemma V.1
• proof
• Lemma V.2