PV1 ⊧ PIRK: Parallel Interval Reachability Kernelcomputes reachable sets of high-dimensional non-linear systems

Tool to efficiently compute reachable sets for general nonlinear systems of extremely high dimensions

Application domain/field

• Reachability analysis
• Nonlinear systems
• Dynamical systems
• Parallelism

Type of tool

Reachability analysis tool

Expected input

• Configuration file
• Dynamic system
• Initial hyper-interval for states and inputs

Format:

• Configuration file: .cfg file
• Dynamical system: .cl file
• Initial hyper-interval: .cl file

The README of the repository describes the expected syntax for each of these files.

Expected output

.raw file which contains the reach pipe of the system

Internals

Uses the acceleration system pFaces.

Comments

There is a Matlab-interface so that users can load/use files generated from PIRK. From the CAV 2020 paper (emphasis our own): "To the best of our knowledge, PIRK is the first and the only tool that can compute reachable sets of general non-linear systems with dimensions beyond the billion."