Quantitative Verification of Kalman Filters
Research output: Contribution to journal › Article › peer-review
Colleges, School and Institutes
Kalman ﬁlters 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 ﬁlter, leading to erroneous estimations. Establishing robustness against such issues can be challenging. We propose novel formal veriﬁcation techniques and software to perform a rigorous quantitative analysis of the eﬀectiveness of Kalman ﬁlters. We present a general framework for modelling Kalman ﬁlter implementations operating on linear discrete-time stochastic systems, and techniques to systematically construct a Markov model of the ﬁlter’s operation using truncation and discretisation of the stochastic noise model. Numerical stability and divergence properties are then veriﬁed using probabilistic model checking. We evaluate the scalability and accuracy of our approach on two distinct probabilistic kinematic models and four Kalman ﬁlter implementations.
|Number of pages||25|
|Journal||Formal Aspects of Computing|
|Publication status||Accepted/In press - 29 Nov 2020|