Skip to main navigation Skip to search Skip to main content

A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning enabled Control Systems

  • Navid Hashemi
  • , Danil Prokhorov
  • , Bardh Hoxha
  • , Georgios Fainekos
  • , Tomoya Yamaguchi
  • , Jyotirmoy V. Deshmukh

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Signal Temporal Logic (STL) has become a popular tool for expressing formal requirements of Cyber-Physical Systems (CPS). The problem of verifying STL properties of neural network-controlled CPS remains a largely unexplored problem. In this paper, we present a model for the verification of Neural Network (NN) controllers for general STL specifications using a custom neural architecture where we map an STL formula into a feed-forward neural network with ReLU activation. In the case where both our plant model and the controller are ReLU-activated neural networks, we reduce the STL verification problem to reachability in ReLU neural networks. We also propose a new approach for neural network controllers with general activation functions; this approach is a sound and complete verification approach based on computing the Lipschitz constant of the closed-loop control system. We demonstrate the practical efficacy of our techniques on a number of examples of learning-enabled control systems.

Original languageEnglish (US)
Title of host publicationICCPS 2023 - Proceedings of the 2023 ACM/IEEE 14th International Conference on Cyber-Physical Systems with CPS-IoT Week 2023
PublisherAssociation for Computing Machinery, Inc
Pages98-109
Number of pages12
ISBN (Electronic)9798400700361
DOIs
StatePublished - May 9 2023
Externally publishedYes
Event14th ACM/IEEE International Conference on Cyber-Physical Systems, with CPS-IoT Week 2023, ICCPS 2023 - San Antonio, United States
Duration: May 9 2023May 12 2023

Publication series

NameICCPS 2023 - Proceedings of the 2023 ACM/IEEE 14th International Conference on Cyber-Physical Systems with CPS-IoT Week 2023

Conference

Conference14th ACM/IEEE International Conference on Cyber-Physical Systems, with CPS-IoT Week 2023, ICCPS 2023
Country/TerritoryUnited States
CitySan Antonio
Period5/9/235/12/23

Keywords

  • Controller
  • Deep Neural Network
  • Lipstchitz constant
  • Model
  • ReLU
  • Reachability
  • Signal Temporal Logic
  • Verification

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Hardware and Architecture

Fingerprint

Dive into the research topics of 'A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning enabled Control Systems'. Together they form a unique fingerprint.

Cite this