Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Configuring Safe Spiking Neural Controllers for Cyber-Physical Systems through Formal Verification

Arkaprava Gupta, Sumana Ghosh, Ansuman Banerjee, Swarup Kumar Mohalik

TL;DR

This work addresses safety guarantees for SNN-based CPS controllers obtained by ANN→SNN conversion. It introduces a MILP-based verification pipeline, solved by Gurobi, to enforce a safe output range while ensuring ANN-level accuracy via a constrained NUMSTEPS search. The authors contribute an iterative bound-tightening procedure to reduce expensive safety verification calls and demonstrate the approach on five benchmark controllers, identifying cases where safety can be certified and providing tightened output ranges when it cannot. The result is a practical methodology for deploying energy-efficient SNN controllers in safety-critical CPS with explicit, verifiable safety bounds.

Abstract

Spiking Neural Networks (SNNs) are a subclass of neuromorphic models that have great potential to be used as controllers in Cyber-Physical Systems (CPSs) due to their energy efficiency. They can benefit from the prevalent approach of first training an Artificial Neural Network (ANN) and then translating to an SNN with subsequent hyperparameter tuning. The tuning is required to ensure that the resulting SNN is accurate with respect to the ANN in terms of metrics like Mean Squared Error (MSE). However, SNN controllers for safety-critical CPSs must also satisfy safety specifications, which are not guaranteed by the conversion approach. In this paper, we propose a solution which tunes the $temporal$ $window$ hyperparameter of the translated SNN to ensure both accuracy and compliance with the safe range specification that requires the SNN outputs to remain within a safe range. The core verification problem is modelled using mixed-integer linear programming (MILP) and is solved with Gurobi. When the controller fails to meet the range specification, we compute tight bounds on the SNN outputs as feedback for the CPS developer. To mitigate the high computational cost of verification, we integrate data-driven steps to minimize verification calls. Our approach provides designers with the confidence to safely integrate energy-efficient SNN controllers into modern CPSs. We demonstrate our approach with experimental results on five different benchmark neural controllers.

Configuring Safe Spiking Neural Controllers for Cyber-Physical Systems through Formal Verification

TL;DR

This work addresses safety guarantees for SNN-based CPS controllers obtained by ANN→SNN conversion. It introduces a MILP-based verification pipeline, solved by Gurobi, to enforce a safe output range while ensuring ANN-level accuracy via a constrained NUMSTEPS search. The authors contribute an iterative bound-tightening procedure to reduce expensive safety verification calls and demonstrate the approach on five benchmark controllers, identifying cases where safety can be certified and providing tightened output ranges when it cannot. The result is a practical methodology for deploying energy-efficient SNN controllers in safety-critical CPS with explicit, verifiable safety bounds.

Abstract

Spiking Neural Networks (SNNs) are a subclass of neuromorphic models that have great potential to be used as controllers in Cyber-Physical Systems (CPSs) due to their energy efficiency. They can benefit from the prevalent approach of first training an Artificial Neural Network (ANN) and then translating to an SNN with subsequent hyperparameter tuning. The tuning is required to ensure that the resulting SNN is accurate with respect to the ANN in terms of metrics like Mean Squared Error (MSE). However, SNN controllers for safety-critical CPSs must also satisfy safety specifications, which are not guaranteed by the conversion approach. In this paper, we propose a solution which tunes the hyperparameter of the translated SNN to ensure both accuracy and compliance with the safe range specification that requires the SNN outputs to remain within a safe range. The core verification problem is modelled using mixed-integer linear programming (MILP) and is solved with Gurobi. When the controller fails to meet the range specification, we compute tight bounds on the SNN outputs as feedback for the CPS developer. To mitigate the high computational cost of verification, we integrate data-driven steps to minimize verification calls. Our approach provides designers with the confidence to safely integrate energy-efficient SNN controllers into modern CPSs. We demonstrate our approach with experimental results on five different benchmark neural controllers.
Paper Structure (21 sections, 13 equations, 5 figures, 4 tables, 5 algorithms)

This paper contains 21 sections, 13 equations, 5 figures, 4 tables, 5 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Artificial Neural Network (ANN) Controller
  4. Spiking Neural Network (SNN) Controller
  5. ANN-SNN Conversion
  6. System Model and Problem Definition
  7. Detailed methodology
  8. Verifying the Safe Range Specification for SNN
  9. MILP Encoding and Safe Range Verification
  10. Encoding the Execution Semantics
  11. Encoding the Safe Range Spec.
  12. Formal Verification
  13. Binary Search for Iterative Bound Tightening
  14. Implementation and Results
  15. Benchmarks
  16. ...and 6 more sections

Figures (5)

  • Figure 1: NN-Controlled CPS
  • Figure 2: An Example SNN
  • Figure 3: Flow Diagram of the Proposed Methodology
  • Figure 4: Outputs of ANN Controller vs. SNN Controller for Linear Inverted Pendulum with increasing NUMSTEPS
  • Figure 5: Given Safe Bounds vs. Bounds obtained for SNN Outputs for Single Pendulum across Timesteps

Theorems & Definitions (1)

  • Definition 1