Signal Temporal Logic Verification and Synthesis Using Deep Reachability Analysis and Layered Control Architecture

TL;DR

This paper introduces a framework combining deep reachability analysis and layered control architecture to verify and synthesize control for STL-specified missions, ensuring safety and reliability with significantly reduced computation time.

Contribution

It presents a novel STL verification and control synthesis method using deep neural networks and layered planning, improving efficiency and robustness over existing approaches.

Findings

Deep neural networks reduce reachability analysis computation time by 1000 times.

The framework successfully verifies STL specifications and performs missions in simulations.

Layered control architecture enhances robustness against unexpected obstacle behaviors.

Abstract

We propose a signal temporal logic (STL)-based framework that rigorously verifies the feasibility of a mission described in STL and synthesizes control to safely execute it. The proposed framework ensures safe and reliable operation through two phases. First, the proposed framework assesses the feasibility of STL by computing a backward reachable tube (BRT), which captures all states that can satisfy the given STL, regardless of the initial state. The proposed framework accommodates the multiple reach-avoid (MRA) problem to address more general STL specifications and leverages a deep neural network to alleviate the computation burden for reachability analysis, reducing the computation time by about 1000 times compared to a baseline method. We further propose a layered planning and control architecture that combines mixed-integer linear programming (MILP) for global planning with model predictive control (MPC) as a local controller for the verified STL. Consequently, the proposed framework can robustly handle unexpected behavior of obstacles that are not described in the environment information or STL, thereby providing reliable mission performance. Our numerical simulations demonstrate that the proposed framework can successfully compute BRT for a given STL and perform the mission.