Volume 40, pp. 187-203, 2013.

Verified stability analysis using the Lyapunov matrix equation

Andreas Frommer and Behnam Hashemi


The Lyapunov matrix equation $AX + XA^* = C$ arises in many applications, particularly in the context of stability of matrices or solutions of ordinary differential equations. In this paper we present a method, based on interval arithmetic, which computes with mathematical rigor an interval matrix containing the exact solution of the Lyapunov equation. We work out two options which can be used to verify, again with mathematical certainty, that the exact solution of the equation is positive definite. This allows to prove stability of the (non-Hermitian) matrix $A$ if we chose $C$ as a negative definite Hermitian matrix. Our algorithm has computational cost comparable to that of a state-of-the art algorithm for computing a floating point approximation of the solution because we can cast almost all operations as matrix-matrix operations for which interval arithmetic can be implemented very efficiently.

Full Text (PDF) [249 KB], BibTeX

Key words

stability analysis, Lyapunov matrix equation, interval arithmetic, Krawczyk's method, verified computation

AMS subject classifications

65F05, 65G20

< Back