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

TL;DR

The paper addresses the robustness and resilience of learning-enabled state estimation systems (LE-SESs) under adversarial perturbations to perception, and proposes a formal verification framework based on a novel PO^2-LTS representation. It formalizes robustness and resilience as constrained optimisation problems, proves NP-completeness, and provides an automated verification algorithm that exhaustively searches attacked paths and computes optimal solutions. The WAMI dynamic-tracking case study with a Kalman filter and CNN perception demonstrates how the framework identifies risks and guides principled redesigns, such as runtime monitoring and joint-KFs, to improve robustness and resilience. Overall, the work delivers a principled methodology for verifying and enhancing safety-critical LE-SESs, with concrete guidance for deployment in real robotic perception-estimation pipelines.

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.

Figures (11)

• Figure 1: The Workflow of Attack on LE-SESs.
• Figure 2: Tree diagram of an unfolding {PO}2-LTS
• Figure 3: The architecture of the vehicle detector.
• Figure 4: Illustration of WAMI system's robustness to the consecutive attack at $k = 5-6$. With increased attack payoff, the deviation is still bounded.
• Figure 5: Illustration of WAMI system's resilience to the one step attack at $k = 8$. The attack payoff $\varphi = 6.49$.