1 of 18

2 of 18

Safety Verification of Autonomous Vehicles based on Signal Temporal Logic (STL) constraints

- Aditya Parameshwaran & Yue Wang

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # 7375

3 of 18

Formal Verification of Off-road Autonomous Vehicles

GOAL:

Formally verify the safety of an off-road autonomous vehicle and develop an autonomous controller based on the safety specifications

RESEARCH OBJECTIVE:

Develop safety verification tools and Model Predictive Control (MPC) based autonomous controller with Signal Temporal Logic (STL) constraints
Conduct offline formal verification of the computed traces to determine the robustness of the controller

SAE International®

SAE 2023 WCX

Paper 2023-01-0113

3

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # 7375

4 of 18

Outline

Research Goal and Objectives
Motivation
Signal Temporal Logic
Cost Function Formulation
Vehicle Model
STL Parser
Mixed Integer Linear Programming
Receding Horizon Control
Results
Future Work

SAE International®

SAE 2023 WCX

Paper 2023-01-0113

4

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # 7375

5 of 18

STL Constraint based Mobile Robot Navigation

Constraints

Objective Function

Vehicle Dynamics

Input and State Bounds

Signal Temporal Logic

+

Optimal Control Input:

Wheel Velocities

Feedback Data

Mixed Integer Linear Programming (MILP) solver

2D Navigation

Safety Region

Offline Verification

Unsafe Region

SAE International®

SAE 2023 WCX

Paper 2023-01-0113

5

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # 7375

6 of 18

Signal Temporal Logic

Introduction

Synthesis

Application

Domain Knowledge

“Natural Language Rules”

Signal Temporal Logic

Logic

Signal

Temporal

“OR”

“AND”

“NOT”

SAE International®

SAE 2023 WCX

Paper 2023-01-0113

6

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # 7375

When developing a feature for an engineering product, be it in robotics, automobiles, ships or even airplanes, the first thing we always begin with is domain knowledge and some critical thinking. This knowledge allows us to synthesize our imagination into something that is realizable. Once I have realized my system, can I begin proposing it to an application. Usually domain knowledge, as my peers and I would talk in would be in some sort of Natural Language, but when it comes down to realizing them, we start writing them down or stating them in equations.

This where Signal Temporal Logic comes in play. It is a bridge that takes that natural language rules that a system should follow and converts into a mathematical, model understanding set of specifications.

Logic operators

Time instances, or varying with time

And a reference signal to which the STL rule/specification is checked

7 of 18

Overview of STL

STL Grammar and Semantics

Predicate

Not

And

Or

Implies

Eventually

Always

Until

SAE International®

SAE 2023 WCX

Paper 2023-01-0113

7

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # 7375

Our reference signal is st . From an application perspective, st could be like the real time velocity of the vehicle, or the distance from the nearest obstacle. It basically changes with time.

If our rule says that he signal st should satisfy specification phi and specification psi, that means that the rule should satisfy phi and psi individually

A more complex one is the always operator, which states that in the time period a to b, the signal should always satisfy the specification phi

The until operator means that the signal should always satisfy phi until it reaches a time period a to b, in which it should satisfy psi.

These come in handy when defining complex interdependent rules. A good example for the until operator could be that the off-road vehicle should always maintain a maximum limit of 20mph as the speed limit, until it reaches an obstacle after which its upper limit should 10mph.

8 of 18

Overview of STL

Graphical Example

Eventually

Always

PROPERTY SATISFIED

AND

PROPERTY SATISFIED

PROPERTY VIOLATED

SAE International®

SAE 2023 WCX

Paper 2023-01-0113

8

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # 7375

9 of 18

Properties of Signal Temporal Logic

Robustness Semantics combined with Safety

And

c

SAE International®

SAE 2023 WCX

Paper 2023-01-0113

9

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # 7375

Robustness is like allowing a range of uncertainty around the given signal to satisfy the specification. We cannot always have the signal to satisfy to the specification exactly and hence in such cases an acceptable robustness value is denoted. This is usually the case when the signal is uncertain.

Rho is the robustness value

Any close to accurate model will have uncertainties and disturbances included in the state equation. These disturbances could lead to the reference signal disobeying our specification in certain conditions. The robustness measure comes handy here if we were to associate a measure value that is still within the acceptable range from the upper or lower bounds. The more or signal deviates from the specification, the less robust our model is.

So when we conduct simulations, we understand whether our STL specifications are too strict or too lenient. Like for instance if I mention in my specifcation that the vehicle speed should always stay within 20 and 25 mph, then I am being too strict and there is a good chance that the model will violate my specification. On the other hand if I mention a larger range, then I could be making my model believe that it is safe to drive at high speeds.

10 of 18

Vehicle Model

Kinematic model for simplicity and to test validity of method
Feedback linearized kinematics model for faster computation^[1]

2D Simplified Kinematic Model

Simplified Vehicle Kinematics (Unicycle Model)

Feedback Linearized Vehicle Model

Discrete-time Linear Vehicle Model

A =

0	0	1	0
0	0	0	1
0	0	0	0
0	0	0	0

, B =

0	0
0	0
1	0
0	1

[1] De Luca et al., Stabilization of the Unicycle Via Dynamic Feedback Linearization,

IFAC Proceedings Volumes, Vol 33, 2000

SAE International®

SAE 2023 WCX

Paper 2023-01-0113

10

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # 7375

11 of 18

Feedback Linearization

Converting the linear control inputs back to nonlinear kinematics

Simulate Non-Linear Dynamics

Linear Vehicle Model

Computed Optimal Control Inputs

Transformation Matrix

SAE International®

SAE 2023 WCX

Paper 2023-01-0113

11

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # 7375

12 of 18

Cost Function Formulation

Cost Function

Control Bounds

State Bounds

Robustness

The aim is to compute optimal control inputs (u*) that maintain positive robustness for the prediction horizon

System Kinematics

The optimal control inputs will be applied to the system model following the linearized system kinematics explained earlier

SAE International®

SAE 2023 WCX

Paper 2023-01-0113

12

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # 7375

13 of 18

STL Parser

From Natural Language to Inequality Equations

Go-To-Goal

Multi-Waypoint Navigation

User Input format:

SAE International®

SAE 2023 WCX

Paper 2023-01-0113

13

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # 7375

14 of 18

Mixed Integer Linear Programming (MILP) Problem

Set of Linear Inequality Equations (L.I.E.)

STL Constraints
System Dynamics
State and Input Bounds

MILP Formulation

Get Goal Coordinates from STL parser

Goal Region L.I.E.

e.g.

G =

1	0	0	0
-1	0	0	0
0	1	0	0
0	-1	0	0

, b =

Get Obstacle Coordinates from STL parser

Like the Goal region, we define an obstacle region polytope as

Obstacle Region L.I.E.

SAE International®

SAE 2023 WCX

Paper 2023-01-0113

14

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # 7375

15 of 18

Receding Horizon Control

Goal Region

e.g.

Goal Region

Obstacle

SAE International®

SAE 2023 WCX

Paper 2023-01-0113

15

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # 7375

16 of 18

Example Simulation 1

Go-To-Goal

Robustness plot

Robustness

STL Specification

"alw ((ev_[04,05] (X(1:2,t) > [0.3;0.5] and X(1:2,t) < [0.5;0.7]))

and X(1:2,t) >~ [1.0;1.2] and X(1:2,t) <~ [1.2;1.7])"

“alw (min_d[t] > 0.05)

Offline Verification

Safety Region

Unsafe Region

SAE International®

SAE 2023 WCX

Paper 2023-01-0113

16

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # 7375

17 of 18

Example Simulation 2

Multi-Waypoint Navigation

Robustness plot

Safety Region

Offline Verification

Unsafe Region

SAE International®

SAE 2023 WCX

Paper 2023-01-0113

17

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # 7375

18 of 18

Contact Info

Thank you

Aditya Parameshwaran, Yue Wang

Clemson University

Clemson, South Carolina

+1 7654186709

aparame@clemson.edu yue6@clemson.edu

Acknowledgment

This work was supported by the Simulation Based Reliability and Safety Program for modeling and simulation of military ground vehicle systems, under the technical services contract No. W56HZV-17-C-0095 with the U.S. Army DEVCOM Ground Vehicle Systems Center (GVSC).

18

Paper 2023-01-0113

SAE International®

SAE 2023 WCX

DISTRIBUTION STATEMENT A. Approved for public release: distribution unlimited. OPSEC # (Pending, NOT approved for Release)