Computer-aided verification of matrix Riccati algorithms

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.