Discrete-Space Analysis of Partial Differential Equations

There are numerous examples that arise and benefit from the reachability analysis problem. In cyber-physical systems (CPS), most dynamic phenomena are described as systems of ordinary differential equations (ODEs). Previous work has been done using zonotopes, support functions, and other geometric data structures to represent subsets of the reachable set and have been shown to be efficient. Meanwhile, a wide range of important control problems are more precisely modeled by partial differential equations (PDEs), even though not much attention has been paid to their reachability analyses. This reason motivates us to investigate the properties of these equations, especially from the reachability analysis and verification perspectives. In contrast to ODEs, PDEs have other space variables that also affect their behaviors and are more complex. In this paper, we study the discrete-space analysis of PDEs. Our ultimate goal is to propose a set of PDE reachability analysis benchmarks, and present preliminary analysis of different dimensional heat equations and wave equations. Finite difference methods (FDMs) are utilized to approximate the derivative at each mesh point with explicit order of errors. FDM will convert the PDE to a system of ODEs depending on the type of boundary conditions and discretization scheme chosen. After that, the problem can be treated as a common reachability problem and relevant conceptions and approaches can be applied and evaluated directly. We used SpaceEx to generate the plots and reachable regions for these equations given inputs and the series of results are shown and analyzed.