PIRK: Parallel Computation of Reachable Sets for General Nonlinear Systems

Reachability analysis is a critical tool for the formal verification of dynamical systems and the synthesis of controllers for them. Due to their computational complexity, many reachability analysis methods are restricted to systems with relatively small dimensions. One significant reason for such limitation is that those approaches, and their implementations, are not designed to leverage parallelism. They use algorithms that are designed to run serially within one compute unit and they can not utilize widely-available high-performance computing (HPC) platforms such as many-core CPUs, GPUs and Cloud-computing services.

PIRK is a tool to efficiently compute reachable sets for general nonlinear systems of extremely high dimensions. PIRK can utilize HPC platforms for computing reachable sets for general high-dimensional non-linear systems. PIRK has been tested on several systems,with state dimensions up to 4 billion. The scalability of PIRK’s parallel implementations is found to be highly favorable.

In PIRK, three parallelized interval reachability analysis methods are introduced PIRK uses simulation-based reachability methods which compute rigorous approximations to reachable sets by integrating one or more systems of ODEs. PIRK is developed in C and OpenCL as an open-source kernel for pFaces. This allows PIRK to be run on a wide range of computing platforms, including CPUs clusters, GPUs, and hardware accelerators from any vendor, as well as cloud-based services like Amazon AWS.

Download

Tool paper and related works

Support