Linear Invariants for Linear Systems

TL;DR

This paper provides a eigenvalue-based sufficient condition for the existence of linear invariants in linear systems, along with a constructive method to synthesize such invariants, facilitating analysis of hybrid systems using linear arithmetic.

Contribution

It introduces a new eigenvalue-based criterion for linear invariants and offers a constructive procedure to synthesize them, advancing verification methods for linear and hybrid systems.

Findings

Eigenvalue condition characterizes existence of k-linear invariants.

Constructive procedure computes k-LI when condition holds.

The gap between necessary and sufficient conditions affects synthesis size.

Abstract

A central question in verification is characterizing when a system has invariants of a certain form, and then synthesizing them. We say a system has a $k$ linear invariant, $k$-LI in short, if it has a conjunction of $k$ linear (non-strict) inequalities -- equivalently, an intersection of $k$ (closed) half spaces -- as an invariant. We present a sufficient condition -- solely in terms of eigenvalues of the $A$-matrix -- for an $n$-dimensional linear dynamical system to have a $k$-LI. Our proof of sufficiency is constructive, and we get a procedure that computes a $k$-LI if the condition holds. We also present a necessary condition, together with many example linear systems where either the sufficient condition, or the necessary is tight, and which show that the gap between the conditions is not easy to overcome. In practice, the gap implies that using our procedure, we synthesize $k$-LI for a larger value of $k$ than what might be necessary. Our result enables analysis of continuous and hybrid systems with linear dynamics in their modes solely using reasoning in the theory of linear arithmetic (polygons), without needing reasoning over nonlinear arithmetic (ellipsoids).