Reachability Analysis for One Dimensional Linear Parabolic Equations

Partial differential equations (PDEs) mathematically describe a wide range of phenomena such as fluid dynamics, or quantum mechanics. Although great achievements have been accomplished in the field of numerical methods for solving PDEs, from a safety verification (or falsification) perspective, methods are still needed to verify (or falsify) a system whose dynamics is specified as a PDE that may depend not only on space, but also on time. As many cyber-physical systems (CPS) involve sensing and control of physical phenomena modeled as PDEs, reachability analysis of PDEs provides novel methods for safety verification and falsification. As a first step to address this challenging problem, we propose a reachability analysis approach leveraging the well-known Galerkin Finite Element Method (FEM) for a class of one-dimensional linear parabolic PDEs with fixed but uncertain inputs and initial conditions, which is a subclass of PDEs that is useful for modeling, for instance, heat flows. In particular, a continuous approximate reachable set of the parabolic PDE is computed using linear interpolation. Since a complete conservativeness is hardly achieved by using the approximate reachable set, to enhance the conservativeness, we investigate the error bound between the numerical solution and the exact analytically unsolvable solution to bloat the continuous approximate reachable set. This bloated reachable set is then used for safety verification and falsification. In the case that the safety specification is violated, our approach produces a numerical trace to prove that there exists an initial condition and input that lead the system to an unsafe state.