Abstract
We study for the first time the verification problem on learning-enabled state estimation systems for robotics, which use Bayes filter for localisation, and use deep neural network to process sensory input into observations for the Bayes filter. Specifically, we are interested in a robustness property of the systems: given a certain ability to an adversary for it to attack the neural network without being noticed, whether or not the state estimation system is able to function with only minor loss of localisation precision? For verification purposes, we reduce the state estimation systems to a novel class of labelled transition systems with payoffs and partial order relations, and formally express the robustness property as a constrained optimisation objective. Based on this, practical verification algorithms are developed. As a major case study, we work with a real-world dynamic tracking system that uses a Kalman filter (a special case of the 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 robustness of the WAMI tracking system but also provide useful counterexamples.
Original language | English |
---|---|
Title of host publication | International Conference on Intelligent Robots and Systems (IROS) |
Pages | 7336-7343 |
Number of pages | 8 |
DOIs | |
Publication status | Published - 24 Oct 2020 |
Event | 2020 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) - Las Vegas, NV, USA Duration: 24 Oct 2020 → 24 Jan 2021 |
Conference
Conference | 2020 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) |
---|---|
Period | 24/10/20 → 24/01/21 |