Quantitative verification of 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 or modelling errors may lead to divergenceof 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 analysisof the effectiveness of Kalman filters. We present a general framework for modelling Kalman filterimplementations 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 stochasticnoise model. Numerical stability and divergence properties are then verified using probabilistic model checking. We evaluate the scalability and accuracy ofour approach on two distinct probabilistic kinematic models and four Kalman filter implementations.