## Abstract

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 language | English |
---|---|

Title of host publication | 2019 IEEE 58th Conference on Decision and Control, CDC 2019 |

Publisher | IEEE |

Pages | 8073-8078 |

Number of pages | 6 |

ISBN (Electronic) | 9781728113982 |

DOIs | |

Publication status | Published - Dec 2019 |

MoE publication type | A4 Article in a conference publication |

Event | IEEE Conference on Decision and Control - Nice, France Duration: 11 Dec 2019 → 13 Dec 2019 Conference number: 58 |

### Publication series

Name | Proceedings of the IEEE Conference on Decision and Control |
---|---|

Volume | 2019-December |

ISSN (Print) | 0743-1546 |

### Conference

Conference | IEEE Conference on Decision and Control |
---|---|

Abbreviated title | CDC |

Country/Territory | France |

City | Nice |

Period | 11/12/2019 → 13/12/2019 |