Certified Reachable Sets for Nonlinear Reaction--Diffusion Systems
For researchers in formal verification and control of PDE systems, this provides a first method to compute certified reachable sets for nonlinear reaction-diffusion PDEs with parametric uncertainties.
The paper addresses reachability analysis for nonlinear reaction-diffusion PDEs with parametric uncertainties, a problem that remains underexplored due to infinite-dimensional state spaces. It proposes a framework combining FEM, POD, and set-based reachability to compute certified over-approximations of reachable sets, with explicit error bounds that hold uniformly over parameter sets.
Reachability analysis for dynamical systems seeks to compute a set containing all reachable states at a given time. Compared to ordinary differential equations (ODEs), the analysis of nonlinear reaction--diffusion PDEs with parametric uncertainties remains largely underexplored, due to the infinite-dimensional state space and the variety of solutions under different parameters. We address this through a three-step procedure: 1) Finite Element Methods (FEM)s to discretise the space and generate a finite-dimensional FEM-based model, 2) Proper Orthogonal Decomposition (POD) to build a Reduced-Order Model (ROM), and 3) set-based reachability-analysis methods applied to the ROM. We propose a framework that enables us to derive explicit upper bounds on the approximation errors introduced at each stage of the pipeline. In particular, we quantify the discrepancy between trajectories of the original PDE and those of the FEM-based discretization, as well as the error between the FEM-based model and the reduced-order model. Importantly, these bounds are shown to hold uniformly over the considered set of parameters. By combining these error estimates, we obtain an over-approximation of the reachable set of the original PDE. The approach is illustrated on the Allen--Cahn equation and a logistic growth PDE.