Quantitative verification of Kalman filters

Alexandros Evangelidis, David Parker

Research output: Contribution to journalArticlepeer-review

50 Downloads (Pure)


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.

Original languageEnglish
Pages (from-to)669-693
JournalFormal Aspects of Computing
Issue number4-5
Early online date5 Feb 2021
Publication statusE-pub ahead of print - 5 Feb 2021

Bibliographical note

Funding Information:
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.

Publisher Copyright:
© 2021, British Computer Society.


  • Kalman filter
  • Probabilistic model checking
  • Quantitative verification

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science


Dive into the research topics of 'Quantitative verification of Kalman filters'. Together they form a unique fingerprint.

Cite this