IMPaCT Software Tool
IMPaCT: Interval MDP Parallel Construction for Controller Synthesis of Large-Scale Stochastic Systems
IMPaCT is an open-source software tool for the parallelised 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-while-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.
The GitHub repository for IMPaCT can be found here, to use IMPaCT you can use the docker image, the automated installation instructions (tested on Ubuntu 22.04), or manually install the tool yourself following the installation guide. You can also find some useful videos for installing and understanding IMPaCT below.