1 of 27

Synthesis and Verification of Neural Feedback Controllers for Temporal Logic Tasks

Georgios Fainekos�Toyota NA R&D

May 2024 @ 1st International Conference on Neuro-symbolic Systems (NeuS)

The views, opinions and technical results presented here are those of myself and my co-authors as subject matter experts, and they do not reflect the official policy or position of Toyota (or any of its member companies). The presenter are solely responsible for the accuracy and validity of the information presented.

2 of 27

Research & Development within TMNA

Advancing R&D to discover better ways of moving people, goods and information

2

FRD

Future mobility

CPS group

MRD

ERD

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

3 of 27

Our research focus

3

② Planning and control of heterogeneous multi-agent systems

③ Human-robot interaction (planning, communication, coordination)

① Requirements, verification, validation, testing, certification

Closed-loop CPS

Machine learning enabled CPS

Fundamental research on risk-aware autonomous systems with mathematical guarantees on functionality and performance under uncertainty.

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

4 of 27

Transitioning to a mobility company : Woven city

4

https://youtu.be/vbzI9ixE_Q0?si=Io5WD8xH2xiZTzea&t=91

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

5 of 27

Problem: Synthesis of NN controllers from formal requirements

5

Perception/Control

Sensors

Environment

Vehicle

  • Requirement 1
  • Requirement 2
  • …
  • Requirement n

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

6 of 27

Example: Safe ADAS

6

 

ego car

lead car

Requirement: if the lead vehicle in your lane has velocity greater than 10 km/hr and the distance from the lead vehicle is at least dm and at most dM , then the ego can always maintain a safe distance in the next 3 sec.

 

  1. Hekmatnejad et. al., Encoding and Monitoring Responsibility Sensitive Safety (RSS) Rules for Automated Vehicles in Signal Temporal Logic, ACM-IEEE MEMOCODE 2019
  2. Maierhofer et. al., Formalization of Interstate Traffic Rules in Temporal Logic. IV 2020
  3. Sun et. al., LawBreaker: An Approach for Specifying Traffic Laws and Fuzzing Autonomous Vehicles, ASE 2022
  4. Reimann et. al., Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance, arxiv 2024.03

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

7 of 27

Robust Semantics

  •  

7

 

Complexity based on dynamic programming:

O(|φ| |τ| c), where c = max 0≤j≤|τ|, I∈T(φ) |[j, max J(j, I)]|

Fainekos, Pappas. Robustness of temporal logic specifications. In FATES/RV 2006

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

8 of 27

Example Robustness

8

 

 

r

 

 

r

 

 

 

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

9 of 27

Closed loop system with FNN controller

  •  

9

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

10 of 27

Problem Formulation

  •  

10

Problem 1

 

Shakiba Yaghoubi �(now at Motional)

Challenges:

  1. Non-differentiable cost (loss) function
  2. Infinite operating domain X0

Yaghoubi & Georgios, Worst-case Satisfaction of STL Specifications Using Feedforward Neural Network Controllers: A Lagrange Multipliers Approach, EMSOFT 2019

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

11 of 27

 

  •  

11

 

Problem 2

* Dimitri P Bertsekas. 2019. REINFORCEMENT LEARNING AND OPTIMAL CONTROL. Athena Scientific.

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

12 of 27

 

12

 

​

​

 

 

 

 

Reminder: Robust Semantics

 

  • The robustness function, and the min function are non differentiable, so we need to approximate them.

​

​

​

*Yash Vardhan Pant, Houssam Abbas, and Rahul Mangharam. 2017. Smooth operator: Control using the smooth robustness of temporal logic. CCTA

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

13 of 27

 

  •  

13

Problem 3

 

 

* To mitigate the impact of vanishing gradients

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

14 of 27

 

  •  

14

 

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

15 of 27

From requirements’ robustness to NN

15

Theorem

 

 

 

 

Hashemi et. al., A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning-Enabled Control Systems, ICCPS 2023

 

Navid Hashemi

(USC)

Jyo Deshmukh�(USC)

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

16 of 27

Benefit? Use standard NN reachability tools

16

We can do requirements verification over NN-CPS using standard reachability analysis tools.

 

 

Robustness Range

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

*

Example reachability tools:

CROWN, POLAR, Sherlock, Veritex, NNV, …

NNV

Exact-star based reachability

Approx-star based reachability

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

17 of 27

Additional benefit: Probabilistic reachability

17

Uncertainty

Sensing is noisy.

ego car

lead car

Hoang-Dung Tran

(UNL)

Sungwoo Choi

(UNL)

Tran et. al., Quantitative verification for neural networks using probstars, HSCC 2023

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

18 of 27

Quantitative verification of NN (no TL specs)

18

 

 

 

 

 

 

 

 

Git: https://github.com/V2A2/StarV

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

19 of 27

Key points: Quantitative verification of NN

  •  

19

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

20 of 27

Better approximation for min/max?

20

ReLU

softplus

swish

Navid

Hashemi

(USC)

Jyo

Deshmukh�(USC)

 

 

 

 

 

 

 

Samuel

Williams

(USC)

Hashemi et. al., LB4TL: A Smooth Semantics for Temporal Logic to Train Neural Feedback Controllers, ADHS 2024

Lemma

 

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

21 of 27

Scaling up: drop samples from gradient

21

Navid

Hashemi

(USC)

Jyo

Deshmukh�(USC)

Hashemi et. al., Scaling Learning based Policy Optimization for Temporal Tasks via Dropout, arxiv 2024 (under review)

 

Include Critical Time in Sampling

 

 

. . .

 

 

 

 

 

Unsafe set

 

 

 

 

 

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

22 of 27

 

Model:

 

 

Network of Dubins Casrs:

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

23 of 27

Outro

23

24 of 27

Closing remarks

  • Temporal logic requirements provide a feasible path for symbolically encoding safety requirements in data-driven systems
  • FFNN controller synthesis for reactive and mid-horizon tasks is now possible
  • Challenging research problems:
    • NN repair after failed verification
    • RNN synthesis under complex TL specifications
    • Are these methods useful beyond NN-CPS?

24

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

25 of 27

Progressing our mission on all fronts*, **

25

Testing and �assurance

methods /

Security /�Digital twin

Global planner:

Task assignment and path planning

Environment

Mapping

To Graph

Abstractions through learning

Considering:

- Traffic flow,

- Capacity,

- Corridor Dim.

- Priority Zones

Hospital Floor Plan

Environment Abstractions

Local planner: Communication and motion planning

Low-level Control: �Risk-aware trust-based safety

Monitoring: �Anomaly detection

Perception & predictions: �Uncertainty quantification for data driven models

Human-robot teaming

Natural language

* my perspective ☺

Learning Workflows

Closing the loop at the appropriate level

** many times with collaborative institutions

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

26 of 27

26

Thank you!

Questions?

?

ProbStar: https://github.com/V2A2/StarV

Acknowledgements (for this presentation)

Navid

Hashemi

(USC)

Jyo

Deshmukh�(USC)

Samuel

Williams

(USC)

Hoang-Dung �Tran

(UNL)

Sungwoo Choi

(UNL)

Bardh Hoxha

(Toyota)

Danil Prokhorov

(Toyota)

Tomoya Yamaguchi

(Toyota)

Hideki Okamoto

(Toyota)

Shakiba Yaghoubi �(now at Motional)

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA

27 of 27

List of references

  1. Yaghoubi & Georgios, Worst-case Satisfaction of STL Specifications Using Feedforward Neural Network Controllers: A Lagrange Multipliers Approach, EMSOFT 2019
  2. Hashemi, Hoxha, Yamaguchi, Prokhorov, Fainekos & Deshmukh, A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning-Enabled Control Systems, ICCPS 2023
  3. Tran, Choi, Okamoto, Hoxha, Fainekos & Prokhorov, Quantitative verification for neural networks using probstars, HSCC 2023
  4. Hashemi, Williams, Hoxha, Prokhorov, Fainekos & Deshmukh, LB4TL: A Smooth Semantics for Temporal Logic to Train Neural Feedback Controllers, ADHS 2024
  5. Hashemi, Hoxha, Prokhorov, Fainekos & Deshmukh, Scaling Learning based Policy Optimization for Temporal Tasks via Dropout, arxiv 2024 (under review)

​

27

TOYOTA RESEARCH INSTITUTE OF NORTH AMERICA