publications

2024

1. Computer-assisted proofs of non-reachability for linear finite-dimensional control systems

   Ivan Hasenohr, Camille Pouchol, Yannick Privat, and Christophe Zhang

   Mar 2024

   Abs Bib URL PDF

   It is customary to design a control 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 finite-dimensional linear control system with compact constraints avoids a chosen unsafe set at a chosen final time T. 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 control problem. Second, computations lead to roundoff errors, which are dealt with by means of interval arithmetic. The control of both error types then leads 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.

   @unpublished{HPPZ2024,
     title = {{Computer-assisted proofs of non-reachability for linear finite-dimensional control systems}},
     author = {Hasenohr, Ivan and Pouchol, Camille and Privat, Yannick and Zhang, Christophe},
     url = {https://hal.science/hal-04523794},
     note = {working paper or preprint},
     year = {2024},
     month = mar,
     keywords = {linear control systems ; controllability under constraints ; computer-assisted proofs ; interval arithmetic},
     hal_id = {hal-04523794},
     hal_version = {v1},
   }