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

PIRK is an open-source tool and can be downloaded from its GitHub repository. PIRK requires the acceleration ecosystem, pFaces, which can be downloaded from here.

Tool paper and related works

  • A. Devonport$, M. Khaled, M. Arcak, M. Zamani. PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems. 32nd Conference on Computer Aided Verification (CAV), July 2020.

  • M. Khaled, and M. Zamani. pFaces: An Acceleration Ecosystem for Symbolic Control. 22nd ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2019), April 16-18, 2019, Montreal, Canada.

Support

Please report any problems/bugs you face while installing and running PIRK to Mahmoud Khaled.