Quantitative Verification of Numerical Stability for Kalman Filters
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.
This work has been partially supported by an EPSRC-funded Ph.D. studentship (award ref: 1576386) and the PRINCESS project (contract FA8750-16-C-0045) funded by the DARPA BRASS programme.
- 1.Math - Commons-Math: The Apache Commons Mathematics Library. http://commons.apache.org/math/
- 2.Anderson, B., Moore, J.: Optimal Filtering. Dover Books on Electrical Engineering. Dover Publications, New York (2012)Google Scholar
- 5.Battin, R.H.: Astronautical Guidance. McGraw-Hill, New York (1964). Electronic sciencesGoogle Scholar
- 6.Bertsekas, D., Tsitsiklis, J.: Introduction to Probability. Athena Scientific, Athena Scientific optimization and computation series (2008)Google Scholar
- 7.Bierman, G.J.: Factorization Methods for Discrete Sequential Estimation (1977)Google Scholar
- 21.Moulin, M., Gluhovsky, L., Bendersky, E.: Formal verification of maneuvering target tracking. In: AIAA Guidance, Navigation, and Control Conference and Exhibit (2003). https://doi.org/10.2514/6.2003-5716
- 22.R. Gamboa, J. Cowles, J.V.B.: On the verification of synthesized kalman filters. In: 4th International Workshop on the ACL2 Theorem Prover and Its Applications (2003)Google Scholar
- 27.Supporting material. www.prismmodelchecker.org/files/fm19kf/