Computer-aided verification of matrix Riccati algorithms

Vassilios A. Tsachouridis, Georgios Giantamidis

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review


This paper presents a preliminary computer-aided reachability analysis method for the formal verification of matrix iterative algorithms, used for the numerical solution of the discrete time algebraic Riccati equation (DARE). Combining existing theoretical results with an affine arithmetic computational framework, it is illustrated how algorithmic dynamics can be formally analysed a priori over predefined sets of DARE data. Two representative algorithms are used as paradigms: a) The iteration of the respective difference matrix Riccati equation and b) the Newton-Raphson algorithm, applied to an equivalent vector Riccati equation. For the first algorithm, the computer-aided reachability approach is used to assess convergence to desired accuracy levels, and computational behaviour of the algorithm's dynamics. For the Newton-Raphson algorithm, the reachability analysis is focused only on the convergence of the algorithm. At present, the method is practical for low dimensional problems and it is demonstrated via numerical examples using a custom made affine arithmetic reachability tool.

Original languageEnglish
Title of host publication2019 IEEE 58th Conference on Decision and Control, CDC 2019
Number of pages6
ISBN (Electronic)9781728113982
Publication statusPublished - Dec 2019
MoE publication typeA4 Article in a conference publication
EventIEEE Conference on Decision and Control - Nice, France
Duration: 11 Dec 201913 Dec 2019
Conference number: 58

Publication series

NameProceedings of the IEEE Conference on Decision and Control
ISSN (Print)0743-1546


ConferenceIEEE Conference on Decision and Control
Abbreviated titleCDC


Dive into the research topics of 'Computer-aided verification of matrix Riccati algorithms'. Together they form a unique fingerprint.

Cite this