publications

2025

1. Computer-assisted proofs of non-reachability for linear parabolic PDEs under bounded control constraints

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

   Nov 2025

   Abs Bib URL PDF

   Analysing reachability associated to a control system is a subtle issue, especially for infinite-dimensional dynamics, and when controls are subject to bounded constraints. We develop a computer-assisted framework for establishing non-reachability in linear parabolic PDEs governed by strongly elliptic operators, extending recent finite-dimensional techniques introduced in [Has+2025] to the PDE setting. The non-reachability of a given target is shown to be equivalent to proving that a properly defined dual functional takes negative values. Our approach combines rigorous numerics with explicit convergence estimates for discretisations of the adjoint equation, ensuring mathematically certified results with tight error bounds. We demonstrate the wide applicability of our framework on Laplacian-driven control systems, showcasing its accuracy and reliability under various types of control constraints.

   @unpublished{hasenohr:hal-05357694,
     title = {{Computer-assisted proofs of non-reachability for linear parabolic PDEs under bounded control constraints}},
     author = {Hasenohr, Ivan and Pouchol, Camille and Privat, Yannick and Zhang, Christophe},
     url = {https://hal.science/hal-05357694},
     note = {Preprint},
     year = {2025},
     month = nov,
     keywords = {linear control systems ; heat equation ; bounded constraints on the control ; non-reachability ; minimal times of reachability ; computer-assisted proof ; Rounding errors},
     hal_id = {hal-05357694},
     hal_version = {v1},
   }

2. Computer-Assisted Proofs of Nonreachability for Finite-Dimensional Linear Control Systems

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

   SIAM Journal on Control and Optimization Sep 2025

   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 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 discretization. We thus provide explicit, fine discretization 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 nonreachability 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.

   @article{HPPZ2025,
     author = {Hasenohr, Ivan and Pouchol, Camille and Privat, Yannick and Zhang, Christophe},
     title = {Computer-Assisted Proofs of Nonreachability for Finite-Dimensional Linear Control Systems},
     journal = {SIAM Journal on Control and Optimization},
     volume = {63},
     number = {5},
     pages = {3272-3296},
     year = {2025},
     month = sep,
     doi = {10.1137/24M1658711},
     url = {https://doi.org/10.1137/24M1658711},
     eprint = {https://doi.org/10.1137/24M1658711},
     keywords = {linear control systems ; controllability under constraints ; computer-assisted proofs ; interval arithmetic},
   }