Computer-assisted proof of non-reachability for linear systems in finite dimension

It is customary to design a controlled system in such a way that, whatever the chosen control satisfying the constraints, the system does not enter so-called unsafe regions. This work introduces a general computer-assisted methodology to prove that a given linear finite-dimensional control systems with compact constraints avoids a chosen unsafe set. Relying on support hyperplanes, we devise a functional such that the property of interest is equivalent to finding a point at which the functional is negative. Actually evaluating the functional first requires time-discretisation. We thus provide explicit, fine discretisation estimates for various types of matrices underlying the controlled problem. Second, computations lead to roundoff errors, which are dealt with by means of interval arithmetic. The control of both error types then lead to rigorous, computer-assisted proofs of non-reachability of the unsafe set. We illustrate the applicability and flexibility of our method in different contexts featuring various control constraints, unsafe sets, types of matrices and problem dimensions.

SICON