Quantitative verification of numerical stability for Kalman filters

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

Standard

Quantitative verification of numerical stability for Kalman filters. / Evangelidis, Alexandros; Parker, Dave.

Formal Methods – The Next 30 Years: Third World Congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings. Springer, 2019. (Lecture Notes in Computer Science; Vol. 11800).

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

Harvard

Evangelidis, A & Parker, D 2019, Quantitative verification of numerical stability for Kalman filters. in Formal Methods – The Next 30 Years: Third World Congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11800, Springer, 23rd International Symposium on Formal Methods (FM'19), Porto, Portugal, 7/10/19. https://doi.org/10.1007/978-3-030-30942-8_26

APA

Evangelidis, A., & Parker, D. (2019). Quantitative verification of numerical stability for Kalman filters. In Formal Methods – The Next 30 Years: Third World Congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings (Lecture Notes in Computer Science; Vol. 11800). Springer. https://doi.org/10.1007/978-3-030-30942-8_26

Vancouver

Evangelidis A, Parker D. Quantitative verification of numerical stability for Kalman filters. In Formal Methods – The Next 30 Years: Third World Congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings. Springer. 2019. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-30942-8_26

Author

Evangelidis, Alexandros ; Parker, Dave. / Quantitative verification of numerical stability for Kalman filters. Formal Methods – The Next 30 Years: Third World Congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings. Springer, 2019. (Lecture Notes in Computer Science).

Bibtex

@inproceedings{5dea2b3f3103443eb9f18bd164ba48d1,
title = "Quantitative verification of numerical stability for Kalman filters",
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{\textquoteright}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. ",
author = "Alexandros Evangelidis and Dave Parker",
year = "2019",
month = sep
day = "23",
doi = "10.1007/978-3-030-30942-8_26",
language = "English",
isbn = "9783030309411",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
booktitle = "Formal Methods – The Next 30 Years",
note = "23rd International Symposium on Formal Methods (FM'19) ; Conference date: 07-10-2019 Through 11-10-2019",

}

RIS

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.

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

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 -