IMPaCT: Interval MDP Parallel Construction for Controller Synthesis of Large-Scale Stochastic Systems

TL;DR

IMPaCT tackles the challenge of verifying and synthesizing controllers for large-scale stochastic systems by constructing finite interval abstractions (IMCs/IMDPs) and applying interval iteration to guarantee convergence for infinite-horizon specifications. The tool exploits adaptive parallelism via AdaptiveCpp SYCL to mitigate the curse of dimensionality, enabling scalable construction of IMDPs and parallelized controller synthesis on CPUs and GPUs. It offers a full pipeline from finite abstraction through verification/synthesis, with robust handling of disturbances and noise distributions, and supports both LP-based and sorting-based GPU approaches. Benchmarking on ARCH-like case studies, including up to 14D, demonstrates substantial speedups and confirms the method’s practicality for safety-critical applications while providing open-source availability.

Abstract

This paper is concerned with developing a software tool, called IMPaCT, for the parallelized verification and controller synthesis of large-scale stochastic systems using interval Markov chains (IMCs) and interval Markov decision processes (IMDPs), respectively. The tool serves to (i) construct IMCs/IMDPs as finite abstractions of underlying original systems, and (ii) leverage interval iteration algorithms for formal verification and controller synthesis over infinite-horizon properties, including safety, reachability, and reach-avoid, while offering convergence guarantees. IMPaCT is developed in C++ and designed using AdaptiveCpp, an independent open-source implementation of SYCL, for adaptive parallelism over CPUs and GPUs of all hardware vendors, including Intel and NVIDIA. IMPaCT stands as the first software tool for the parallel construction of IMCs/IMDPs, empowered with the capability to leverage high-performance computing platforms and cloud computing services. Specifically, parallelism offered by IMPaCT effectively addresses the challenges arising from the state-explosion problem inherent in discretization-based techniques applied to large-scale stochastic systems. We benchmark IMPaCT on several physical case studies, adopted from the ARCH tool competition for stochastic models, including a 2-dimensional robot, a 3-dimensional autonomous vehicle, a 5-dimensional room temperature system, and a 7-dimensional building automation system. To show the scalability of our tool, we also employ IMPaCT for the formal analysis of a 14-dimensional case study.

Figures (4)

• Figure 1: 2D Robot case study fulfilling reachability and reach-avoid properties with different noise realizations. The green and red boxes are target and avoid regions, respectively.
• Figure 2: 3D Autonomous Vehicle case study fulfilling reach-while-avoid property, with different noise realizations, starting from an initial condition $[3;-3;0.6]$. The green and red boxes are target and avoid regions, respectively.
• Figure 3: 3D Room Temperature fulfilling safety properties over $10$ time steps, with different noise realizations, starting from an initial condition $[21;21;21]$.
• Figure 4: 4D Building Automation System fulfilling safety properties within $10$ time steps, with $5$ different noise realizations, starting from an initial condition $[19; 20;36;36]$.

Theorems & Definitions (10)

• Definition 2.1: dt-SCS
• Definition 2.2: Continuous-Space MDPs
• Definition 3.1: IMDPs
• Definition 3.2: Specifications
• Remark 3.3
• Remark 4.1
• Remark 5.1
• Remark 5.2
• Remark 6.1
• Remark 6.2