CAFF Problem Instance: Heat3D
The Heat3D benchmark is a spatially discretized version of the heat equation partial differential equation (PDE) in three dimensions. One way to analyze PDEs is to discretize space in a mesh resulting in a system of ordinary differential equations (ODEs), where each variable in the system is a mesh point. Depending on the granularity of discretization, you can adjust the number of variables in the ODE system. This system has no switching or inputs, and serves to evaluate one aspect of scalability, namely the number of system dimensions. It is an academic example, although modifications such as external inputs or more complicated specs can be added in the future to further stress the tools. This benchmark was used in [1], and is based on a 2D version originally described and evaluated in [2, 3] .
The problem is to find the maximum temperature, TempMax, reached at the center of a 1.0 x 1.0 x 1.0 block, where one edge of the block is initially heated. This can be converted to a safety problem by checking that TempMax + delta is not reachable whereas TempMax - delta is reachable, for some small delta like 1e-4.
All of the sides of the block are insulated except the x=1.0 edge, which allows for heat exchange with the ambient environment with a heat exchange constant of 0.5. A heated initial region is present in the region where x = [0.0, 0.4], y = [0.0, 0.2], and z = [0.0, 0.1]. The entire initial heated region is the same temperature, which is nondeterministic and chosen in the range 0.9 to 1.1, with the rest of material initially at temperature 0.0. The system dynamics is given by the heat equation PDE u_t = \alpha^2(u_{xx} + u_{yy} + u_{zz}), where \alpha = 0.01 is the diffusivity of the material.
A linear state space model of the system is obtained using the semi-finite difference method, discretizing the block with an m x m x m grid. This results in an m^3-dimensional linear system describing the evolution of the temperature at each mesh point.
Due to the initially heated region, we expect the temperature at the center of the block to first increase, and then decrease due to the heat loss along the x=1 edge. Further, there may be error due to the space discretization step, so if m is too small, the model does not accurately predict the behavior of the PDE. This motivates the need for analyzing a higher dimensional version of the benchmark. We suggest a time bound of T=40 and a step size of 0.02 (2000 steps).
A python3 script is provided to create the A matrix and run simulations. There are five suggested sizes, roughly each one order of magnitude apart in terms of the number of dimensions:
5x5x5 (125 dimensions). Note for this one the initial set is modified to be heated when z = [0.0, 0.2] (single mesh point), since that is the best we can do with this granularity. Maximum temp: 0.10369885 at time 9.44.
10x10x10 (1000 dimensions). Sim Result: Maximum temp 0.02966356 at time 25.5.
20x20x20 (8000 dimensions). Sim Result: Maximum temp 0.01716509 at time 22.62.
50x50x50 (125000 dimensions)
100x100x100 (1000000 dimensions)
The python3 script to make the dynamics and simulation is available here: http://stanleybak.com/perm/make_heat3d_archcomp.py
[1] Bak, Stanley, Hoang-Dung Tran, and Taylor T. Johnson. "Numerical verification of affine systems with up to a billion dimensions." Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. 2019.
[2] Han, Zhi, and Bruce H. Krogh. "Reachability analysis of large-scale affine systems using low-dimensional polytopes." International Workshop on Hybrid Systems: Computation and Control. Springer, Berlin, Heidelberg, 2006.
[3] Han, Zhi. Formal verification of hybrid systems using model order reduction and decomposition. Diss. PhD thesis, Dept. of ECE, Carnegie Mellon University, 2005.