Quantitative verification of Kalman filters
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 or modelling errors may lead to divergence of the filter, leading to erroneous estimations. 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 and divergence properties are then verified using probabilistic model checking. We evaluate the scalability and accuracy of our approach on two distinct probabilistic kinematic models and four Kalman filter implementations.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Aug 01, 2021
- Source ID
- 10.1007/s00165-020-00529-w
Entities
People
- Alexandros Evangelidis
- David Parker
Organizations
- Defense Advanced Research Projects Agency
- Engineering and Physical Sciences Research Council
- University of Birmingham