Quantitative verification of numerical stability for Kalman filters
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
Authors
Colleges, School and Institutes
Abstract
Kalman filters are widely used for estimating the state of a system based on noisy or inaccurate sensor readings, for example in the control and navigation of vehicles or robots. However, numerical instability may lead to divergence of the filter, and establishing robustness against such issues can be challenging. We propose novel formal verification techniques and software to perform a rigorous quantitative analysis of the effectiveness of Kalman filters. We present a general framework for modelling Kalman filter implementations operating on linear discrete-time stochastic systems, and techniques to systematically construct a Markov model of the filter’s operation using truncation and discretisation of the stochastic noise model. Numerical stability properties are then verified using probabilistic model checking. We evaluate the scalability and accuracy of our approach on two distinct probabilistic kinematic models and several implementations of Kalman filters.
Details
Original language | English |
---|---|
Title of host publication | Formal Methods – The Next 30 Years |
Subtitle of host publication | Third World Congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings |
Publication status | Published - 23 Sep 2019 |
Event | 23rd International Symposium on Formal Methods (FM'19) - Porto, Portugal Duration: 7 Oct 2019 → 11 Oct 2019 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Volume | 11800 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 23rd International Symposium on Formal Methods (FM'19) |
---|---|
Country | Portugal |
City | Porto |
Period | 7/10/19 → 11/10/19 |