2020/01/28 by Alex Devonport, Devonport, Alex, Mahmoud Khaled +5 · 1 citation
Computer Science · Engineering · #Advanced Control Systems Optimization #FOS: Electrical engineering #Formal Methods in Verification #Numerical Methods and Algorithms #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.2001.10635
openalex publication_date 2020/01/28 · openalex created_date 2022/07/26 · openalex updated_date 2026/07/28
Reachability analysis is a critical tool for the formal verification of\ndynamical systems and the synthesis of controllers for them. Due to their\ncomputational complexity, many reachability analysis methods are restricted to\nsystems with relatively small dimensions. One significant reason for such\nlimitation is that those approaches, and their implementations, are not\ndesigned to leverage parallelism. They use algorithms that are designed to run\nserially within one compute unit and they can not utilize widely-available\nhigh-performance computing (HPC) platforms such as many-core CPUs, GPUs and\nCloud-computing services.\n This paper presents PIRK, a tool to efficiently compute reachable sets for\ngeneral nonlinear systems of extremely high dimensions. PIRK has been tested on\nseveral systems, with state dimensions ranging from ten up to 4 billion. The\nscalability of PIRK's parallel implementations is found to be highly favorable.\n