Quantitative verification of numerical stability for Kalman filters

Alexandros Evangelidis, Dave Parker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)
147 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationFormal Methods – The Next 30 Years
Subtitle of host publicationThird World Congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings
PublisherSpringer
Number of pages17
ISBN (Electronic)9783030309428
ISBN (Print)9783030309411
DOIs
Publication statusPublished - 23 Sep 2019
Event23rd International Symposium on Formal Methods (FM'19) - Porto, Portugal
Duration: 7 Oct 201911 Oct 2019

Publication series

NameLecture Notes in Computer Science
Volume11800
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference23rd International Symposium on Formal Methods (FM'19)
Country/TerritoryPortugal
CityPorto
Period7/10/1911/10/19

Fingerprint

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

Cite this