Formal Verification of Robustness and Resilience of Learning-Enabled State Estimation Systems

• URL: http://arxiv.org/abs/2010.08311v4
• Date: Fri, 29 Mar 2024 14:41:08 GMT
• Title: Formal Verification of Robustness and Resilience of Learning-Enabled State Estimation Systems
• Authors: Wei Huang, Yifan Zhou, Gaojie Jin, Youcheng Sun, Jie Meng, Fan Zhang, Xiaowei Huang,
• Abstract summary: We focus on learning-enabled state estimation systems (LE-SESs), which have been widely used in robotics applications. We study LE-SESs from the perspective of formal verification, which determines the satisfiabilty of a system model.
• Score: 20.491263196235376
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: This paper presents a formal verification guided approach for a principled design and implementation of robust and resilient learning-enabled systems. We focus on learning-enabled state estimation systems (LE-SESs), which have been widely used in robotics applications to determine the current state (e.g., location, speed, direction, etc.) of a complex system. The LE-SESs are networked systems, composed of a set of connected components including: Bayes filters for state estimation, and neural networks for processing sensory input. We study LE-SESs from the perspective of formal verification, which determines the satisfiabilty of a system model against the specified properties. Over LE-SESs, we investigate two key properties -- robustness and resilience -- and provide their formal definitions. To enable formal verification, we reduce the LE-SESs to a novel class of labelled transition systems, named {PO}^2-LTS in the paper, and formally express the properties as constrained optimisation objectives. We prove that the verification problems are NP-complete. Based on {PO}^2-LTS and the optimisation objectives, practical verification algorithms are developed to check the satisfiability of the properties on the LE-SESs. As a major case study, we interrogate a real-world dynamic tracking system which uses a single Kalman Filter (KF) -- a special case of Bayes filter -- to localise and track a ground vehicle. Its perception system, based on convolutional neural networks, processes a high-resolution Wide Area Motion Imagery (WAMI) data stream. Experimental results show that our algorithms can not only verify the properties of the WAMI tracking system but also provide representative examples, the latter of which inspired us to take an enhanced LE-SESs design where runtime monitors or joint-KFs are required. Experimental results confirm the improvement in the robustness of the enhanced design.

Related papers

• Entropy-Regularized Token-Level Policy Optimization for Language Agent Reinforcement [67.1393112206885]
  Large Language Models (LLMs) have shown promise as intelligent agents in interactive decision-making tasks. We introduce Entropy-Regularized Token-level Policy Optimization (ETPO), an entropy-augmented RL method tailored for optimizing LLMs at the token level. We assess the effectiveness of ETPO within a simulated environment that models data science code generation as a series of multi-step interactive tasks.
  arXiv  Detail & Related papers  (2024-02-09T07:45:26Z)
• RLEEGNet: Integrating Brain-Computer Interfaces with Adaptive AI for Intuitive Responsiveness and High-Accuracy Motor Imagery Classification [0.0]
  We introduce a framework that leverages Reinforcement Learning with Deep Q-Networks (DQN) for classification tasks. We present a preprocessing technique for multiclass motor imagery (MI) classification in a One-Versus-The-Rest (OVR) manner. The integration of DQN with a 1D-CNN-LSTM architecture optimize the decision-making process in real-time.
  arXiv  Detail & Related papers  (2024-02-09T02:03:13Z)
• Investigating Robustness in Cyber-Physical Systems: Specification-Centric Analysis in the face of System Deviations [8.8690305802668]
  A critical attribute of cyber-physical systems (CPS) is robustness, denoting its capacity to operate safely. This paper proposes a novel specification-based robustness, which characterizes the effectiveness of a controller in meeting a specified system requirement. We present an innovative two-layer simulation-based analysis framework designed to identify subtle robustness violations.
  arXiv  Detail & Related papers  (2023-11-13T16:44:43Z)
• Physics Inspired Hybrid Attention for SAR Target Recognition [61.01086031364307]
  We propose a physics inspired hybrid attention (PIHA) mechanism and the once-for-all (OFA) evaluation protocol to address the issues. PIHA leverages the high-level semantics of physical information to activate and guide the feature group aware of local semantics of target. Our method outperforms other state-of-the-art approaches in 12 test scenarios with same ASC parameters.
  arXiv  Detail & Related papers  (2023-09-27T14:39:41Z)
• SysNoise: Exploring and Benchmarking Training-Deployment System Inconsistency [55.49469003537601]
  We introduce SysNoise, a frequently occurred but often overlooked noise in the deep learning training-deployment cycle. We measure the impact of SysNoise on 20+ models, comprehending image classification, object detection, instance segmentation and natural language processing tasks. Our experiments revealed that SysNoise could bring certain impacts on model robustness across different tasks and common mitigations like data augmentation and adversarial training show limited effects on it.
  arXiv  Detail & Related papers  (2023-07-01T09:22:54Z)
• Age of Semantics in Cooperative Communications: To Expedite Simulation Towards Real via Offline Reinforcement Learning [53.18060442931179]
  We propose the age of semantics (AoS) for measuring semantics freshness of status updates in a cooperative relay communication system. We derive an online deep actor-critic (DAC) learning scheme under the on-policy temporal difference learning framework. We then put forward a novel offline DAC scheme, which estimates the optimal control policy from a previously collected dataset.
  arXiv  Detail & Related papers  (2022-09-19T11:55:28Z)
• Formalizing and Evaluating Requirements of Perception Systems for Automated Vehicles using Spatio-Temporal Perception Logic [25.070876549371693]
  We present a logic that enables reasoning over perception data using spatial and temporal operators. One major advantage ofSTPL is that it facilitates basic sanity checks on the functional performance of the perception system.
  arXiv  Detail & Related papers  (2022-06-29T02:36:53Z)
• Fingerprint recognition with embedded presentation attacks detection: are we ready? [6.0168714922994075]
  The diffusion of fingerprint verification systems for security applications makes it urgent to investigate the embedding of software-based presentation attack algorithms (PAD) into such systems. Current research did not state much about their effectiveness when embedded in fingerprint verification systems. This paper proposes a performance simulator based on the probabilistic modeling of the relationships among the Receiver Operating Characteristics (ROC) of the two individual systems when PAD and verification stages are implemented sequentially.
  arXiv  Detail & Related papers  (2021-10-20T13:53:16Z)
• An Explainable Machine Learning-based Network Intrusion Detection System for Enabling Generalisability in Securing IoT Networks [0.0]
  Machine Learning (ML)-based network intrusion detection systems bring many benefits for enhancing the security posture of an organisation. Many systems have been designed and developed in the research community, often achieving a perfect detection rate when evaluated using certain datasets. This paper tightens the gap by evaluating the generalisability of a common feature set to different network environments and attack types.
  arXiv  Detail & Related papers  (2021-04-15T00:44:45Z)
• A Novel Anomaly Detection Algorithm for Hybrid Production Systems based on Deep Learning and Timed Automata [73.38551379469533]
  DAD:DeepAnomalyDetection is a new approach for automatic model learning and anomaly detection in hybrid production systems. It combines deep learning and timed automata for creating behavioral model from observations. The algorithm has been applied to few data sets including two from real systems and has shown promising results.
  arXiv  Detail & Related papers  (2020-10-29T08:27:43Z)
• Deep Speaker Embeddings for Far-Field Speaker Recognition on Short Utterances [53.063441357826484]
  Speaker recognition systems based on deep speaker embeddings have achieved significant performance in controlled conditions. Speaker verification on short utterances in uncontrolled noisy environment conditions is one of the most challenging and highly demanded tasks. This paper presents approaches aimed to achieve two goals: a) improve the quality of far-field speaker verification systems in the presence of environmental noise, reverberation and b) reduce the system qualitydegradation for short utterances.
  arXiv  Detail & Related papers  (2020-02-14T13:34:33Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.