{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,27]],"date-time":"2026-01-27T11:24:31Z","timestamp":1769513071928,"version":"3.49.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"4-5","license":[{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"crossref","award":["FA8750-16-C-0045"],"award-info":[{"award-number":["FA8750-16-C-0045"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"crossref","award":["1576386"],"award-info":[{"award-number":["1576386"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 divergence of 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 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 and divergence properties are then verified using probabilistic model checking. We evaluate the scalability and accuracy of our approach on two distinct probabilistic kinematic models and four Kalman filter implementations.<\/jats:p>","DOI":"10.1007\/s00165-020-00529-w","type":"journal-article","created":{"date-parts":[[2021,2,5]],"date-time":"2021-02-05T11:58:29Z","timestamp":1612526309000},"page":"669-693","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Quantitative verification of Kalman filters"],"prefix":"10.1145","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4032-3042","authenticated-orcid":false,"given":"Alexandros","family":"Evangelidis","sequence":"first","affiliation":[{"name":"School of Computer Science, University of Birmingham, Birmingham, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4137-8862","authenticated-orcid":false,"given":"David","family":"Parker","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of Birmingham, Birmingham, United Kingdom"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abdelnour G Chand S Chiu S Kido T (1993) On-line detection and correction of kalman filter divergence by fuzzy logic. In: 1993 American control conference pp 1835\u20131839","DOI":"10.23919\/ACC.1993.4793195"},{"key":"e_1_2_1_2_2_2","volume-title":"Optimal filtering","author":"Anderson BDO","year":"2012"},{"key":"e_1_2_1_2_3_2","unstructured":"Math-Commons-Math: the apache commons mathematics library"},{"key":"e_1_2_1_2_4_2","unstructured":"Battin R.H.: Astronautical guidance. Electronic sciences McGraw-Hill New York (1964)"},{"key":"e_1_2_1_2_5_2","unstructured":"Brown RG Hwang PYC (2012) Introduction to random signals and applied Kalman filtering with MATLAB exercises 4th Edition. Wiley Global Education"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bierman GJ (1975) Measurement updating using the u-d factorization. In: 1975 IEEE conference on decision and control including the 14th symposium on adaptive processes pp 337\u2013346","DOI":"10.1109\/CDC.1975.270702"},{"key":"e_1_2_1_2_7_2","unstructured":"Bierman GJ (1977) Factorization methods for discrete sequential estimation"},{"key":"e_1_2_1_2_8_2","unstructured":"Bucy RS Joseph PD (1968) Processes with applications to guidance. Interscience Publishers New York"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Boland F.M. Nicholson H.: Control of divergence in kalmanfilters. Electron Lett 12 (15) 367\u2013369 (1976)","DOI":"10.1049\/el:19760282"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.5555\/38113"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.5555\/560900"},{"key":"e_1_2_1_2_12_2","volume-title":"Introduction toprobability","author":"Bertsekas DP","year":"2008"},{"issue":"9","key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","first-page":"1259","DOI":"10.2514\/3.6907","article-title":"Fast triangular formulation of the square root filter","volume":"11","author":"Carlson NA","year":"1973","journal-title":"AIAA J"},{"key":"e_1_2_1_2_14_2","volume-title":"Applied state estimation and association","author":"Chang C-B","year":"2016"},{"key":"e_1_2_1_2_15_2","unstructured":"The Analytic\u00a0Sciences Corporation and Arthur Gelb. Applied optimal estimation. The MIT Press (1974)"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"D'Souza C Zanetti R (2018) Information formulation of the udu kalmanfilter. IEEE Tran Aerosp Electron Syst pp 1\u20131","DOI":"10.1109\/TAES.2018.2850379"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Evangelidis A Parker D (2019) Quantitative verification of numerical stability for Kalman filters. In: Proc. 23rd International Symposium on Formal Methods (FM'19) volume 11800 of LNCS pp 425\u2013441. Springer","DOI":"10.1007\/978-3-030-30942-8_26"},{"key":"e_1_2_1_2_18_2","volume-title":"Formal methods for eternal networked software systems (SFM'11), volume 6659 of LNCS, pp 53\u2013113","author":"Forejt V","year":"2011"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","DOI":"10.1002\/9781118984987","volume-title":"Kalman filtering: Theory and practice using MATLAB","author":"Grewal MS","year":"2014","edition":"4"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","DOI":"10.1002\/9780470890042","volume-title":"Advanced Kalman filtering, least squares and modeling: a practical handbook","author":"Gibbs BP","year":"2011"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Ge Q. Shao T. Duan Z. Wen C.: Performance analysis of the kalman filter with mismatched noise covariances. IEEE Trans Autom Control 61 (12) 4014\u20134019 (Dec 2016)","DOI":"10.1109\/TAC.2016.2535158"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Hansson H. Jonsson B.: A logic for reasoning about time and reliability. Formal Asp Comput 6 (5) 512\u2013535 (1994)","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_2_23_2","volume-title":"Stochastic processes and filtering theory","author":"Jazwinski AH","year":"1970"},{"key":"e_1_2_1_2_24_2","volume-title":"Continuous univariate distributions","author":"Johnson NL","year":"1994"},{"key":"e_1_2_1_2_25_2","volume-title":"Linear systems","author":"Kailath T","year":"1980"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Kalman RE (1960) A new approach to linear filtering and predictionproblems. ASME J Basic Eng","DOI":"10.1115\/1.3662552"},{"issue":"6","key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","first-page":"727","DOI":"10.1109\/TAC.1971.1099816","article-title":"Discrete square root filtering: a survey of current techniques","volume":"16","author":"Kaminski P","year":"1971","journal-title":"IEEE Trans Autom Control"},{"key":"e_1_2_1_2_28_2","first-page":"220","volume-title":"Formal methods for performance evaluation, number 4486 in lecture notes in computer science","author":"Kwiatkowska M","year":"2007"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M Norman G Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan G Qadeer S (eds) Proceedings of 23rd international conference on computer aided verification (CAV'11) volume 6806 of LNCS pp 585\u2013591. Springer","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M (2007) Quantitative verification: Models techniques andtools. In: Proceedings of 6th joint meeting of the European software engineering conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE)","DOI":"10.1145\/1295014.1295018"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Rong Li X Jilkov VP (Oct 2003) Survey of maneuvering target tracking. Part i. dynamic models. IEEE Trans Aerosp Electron Syst 39(4):1333\u20131364","DOI":"10.1109\/TAES.2003.1261132"},{"key":"e_1_2_1_2_32_2","volume-title":"Stochastic models, estimation, and control:","author":"Maybeck PS","year":"1982"},{"key":"e_1_2_1_2_33_2","unstructured":"Maybeck PS (1982) Stochastic models: estimation and control: volume 2. Mathematics in science and engineering. Elsevier Science"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Moulin M Gluhovsky L Bendersky E (2003) Formal verification of maneuvering target tracking. AIAA Guidance Navigation and Control Conference and Exhibit","DOI":"10.2514\/6.2003-5716"},{"key":"e_1_2_1_2_35_2","unstructured":"Reid I (2001) Estimation ii"},{"key":"e_1_2_1_2_36_2","unstructured":"Van\u00a0Baalen J Gamboa R Cowles J (2003) On the verification of synthesized kalman filters. In: 4th international workshop on the ACL2 theorem prover and its applications"},{"key":"e_1_2_1_2_37_2","first-page":"301","volume-title":"Certifying optimality of stateestimation programs","author":"Ro\u015fu G","year":"2003"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","DOI":"10.1002\/0470045345","volume-title":"Optimal state estimation: Kalman, H infinity, andnonlinear approaches","author":"Simon D","year":"2006"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1049\/iet-cta.2009.0032"},{"key":"e_1_2_1_2_40_2","unstructured":"Supporting material. www.prismmodelchecker.org\/files\/fm19kf\/"},{"key":"e_1_2_1_2_41_2","unstructured":"Thornton CL (1976) Triangular covariance factorizations for Kalman filtering. PhD thesis University of California at Los Angeles"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.1986.1104128"},{"key":"e_1_2_1_2_43_2","volume-title":"All of statistics: a concise course in statistical inference","author":"Larry Wasserman","year":"2010"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/1039813.1039816"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"publisher","DOI":"10.2514\/4.102776"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00529-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-020-00529-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00529-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-020-00529-w","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,20]],"date-time":"2023-10-20T11:14:22Z","timestamp":1697800462000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-020-00529-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8]]},"references-count":45,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["10.1007\/s00165-020-00529-w"],"URL":"https:\/\/doi.org\/10.1007\/s00165-020-00529-w","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8]]},"assertion":[{"value":"28 February 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 October 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 December 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 February 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}