Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Joonwon Choi, Kartik Anand Pant, Youngim Nam, Henry Hellmann, Karthik Nune, Inseok Hwang

TL;DR

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 is proposed, which can robustly handle unexpected behavior of obstacles that are not described in the environment information or STL, thereby providing reliable mission performance.

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.

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

TL;DR

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 is proposed, which can robustly handle unexpected behavior of obstacles that are not described in the environment information or STL, thereby providing reliable mission performance.

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.
Paper Structure (20 sections, 17 equations, 5 figures, 1 table)

This paper contains 20 sections, 17 equations, 5 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Signal temporal logic (STL)
  4. Backward reachable tube (BRT)
  5. Proposed framework
  6. Framework overview
  7. Deep Reachability-based STL verification using DeepSTLReach
  8. Accommodating MRA problem
  9. Deep reachability analysis
  10. Layered-architecture for planning and control
  11. Global Planning via Mixed-Integer Linear Programming (MILP)
  12. MPC-based Local Planning and Control
  13. Numerical Simulation
  14. Simulation setup
  15. Scenario 1: Unexpected moving obstacle
  16. ...and 5 more sections

Figures (5)

  • Figure 1: Example of conflict
  • Figure 2: Simulation environment and results of Scenario 1. (Left) Scenario 1 map. (Center) Simulation result with $T=8 [s]$. (Right) Runtime assurance of MPC under unexpected environment changes with $T=10[s]$
  • Figure 3: Simulation environment and results of Scenario 2. (Left) Scenario 2 map. (Center) Simulation result with $T=10[s]$. (Right) Simulation result with $T=11[s]$.
  • Figure 4: Simulation environment and results of Scenario 3. (Left) Scenario 3 map. (Right) Simulation result with $T=20s$.
  • Figure 5: (Left) Scenario 1, $T=9[s]$ (Right) Scenario 2, $T=10[s]$

Theorems & Definitions (1)

  • Remark 1