publications

2025

1. PHD THESIS

   Computer-assisted proofs of reachability analysis for linear control systems under bounded constraints

   Ivan Hasenohr

   Nov 2025

   Abs Bib URL PDF

   This thesis is devoted to the reachability of linear control problems subject to bounded control constraints. Using a convex-analytic approach and supporting hyperplanes, we introduce a functional J whose nonnegativity on the state space is equivalent to the reachability of a target set. One key property of J is that it depends exclusively on control constraints and on the solution to the adjoint problem. By means of the proposed functional, we mainly focus on proving the non-reachability of targets, which amounts to finding points at which J is negative. We introduce a computer-assisted method relying on the discretisation and minimisation of J. First, a discretised proxy is minimised to find a negative point. We then bound the discretisation errors using new discretisation-error bounds with explicit constants, and rounding errors thanks to interval arithmetic. Ultimately, this ensures the original functional J’s value is enclosed in a computed interval, whose negativity delivers a computer-assisted proof of the non-reachability of the chosen target. We prove the effectiveness of the method both in the finite- and infinite-dimensional setting: in a first part, we formalise the method and develop discretisation-error bounds for a wide array of finite-dimensional systems and control constraints, and apply it to various examples, providing non-reachability proofs and lower bounds of minimal reachability times. In a second part, we extend the method to the control of linear parabolic equations, with the 1D heat equation and variants thereof as the prime example. By finely estimating constants associated to discretisation errors, we arrive at proofs of non-reachability for targets under realistic constraints. This functional can also be used to prove positive results of reachability: we present ongoing work aiming to compute verified under- and over-approximations of the reachable set.

   @phdthesis{hasenohr:tel-05620744,
     title = {{Computer-assisted proofs of reachability analysis for linear control systems under bounded constraints}},
     author = {Hasenohr, Ivan},
     url = {https://theses.hal.science/tel-05620744},
     number = {2025UNIP7221},
     school = {{Universit{\'e} Paris Cit{\'e}}},
     year = {2025},
     month = nov,
     keywords = {Interval arithmetic ; Computer-Assisted proofs ; Finite- and infinite-Dimensional control systems ; Reachability analysis ; Bounded control constraints ; Linear control systems ; Arithm{\'e}tique d'intervalles ; Preuves assist{\'e}es par ordinateur ; Syst{\`e}mes de dimension finie et infinie ; Atteignabilit{\'e} ; Contr{\^o}le sous contraintes born{\'e}es ; Probl{\`e}mes de contr{\^o}le lin{\'e}aires},
     type = {Theses},
     hal_id = {tel-05620744},
     hal_version = {v1},
   }

2. PREPRINT

   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},
   }

3. SIAM

   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},
   }