TY - GEN
T1 - Quantitative verification of numerical stability for Kalman filters
AU - Evangelidis, Alexandros
AU - Parker, Dave
PY - 2019/9/23
Y1 - 2019/9/23
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85074237533&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-30942-8_26
DO - 10.1007/978-3-030-30942-8_26
M3 - Conference contribution
SN - 9783030309411
T3 - Lecture Notes in Computer Science
SP - 425
EP - 441
BT - Formal Methods – The Next 30 Years
PB - Springer
T2 - 23rd International Symposium on Formal Methods (FM'19)
Y2 - 7 October 2019 through 11 October 2019
ER -