Software Development

 

AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems

AMYTISS is an advanced software tool developed in C++/OpenCL that provides parallel automated controller synthesis for large-scale discrete-time stochastic control systems which is absolutely crucial in many safety-critical applications. This tool allows to:

• build finite Markov decision processes (MDPs) as finite abstractions of given original stochastic systems;

• synthesize automated controllers for the constructed finite MDPs satisfying some high-level specifications (e.g., safety, reachability & reach-avoid).

AMYTISS enjoys high-performance computing (HPC) platforms together with cloud-computing services to mitigate the problem of state-explosion which is always the case in analyzing large-scale stochastic systems. This tool significantly improves performances w.r.t. computation time and memory usage by parallel execution in different heterogeneous computing platforms including CPUs, GPUs and hardware accelerators (HWAs).

Download

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

Tool paper

• A. Lavaei, M. Khaled, S. Soudjani, and M. Zamani, AMYTISS: PArallelized AutoMated Controller SYnthesis for Large-Scale STochastIc SystemS, 32nd International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science 12225, pp. 461-474, Springer, 2020. (acceptance rate: 27%)

• A. Lavaei, M. Khaled, S. Soudjani, and M. Zamani, AMYTISS: A Parallelized Tool on Automated Controller Synthesis for Large-Scale Stochastic Systems, 23rd ACM International Conference on Hybrid Systems: Computation and Control (HSCC), 2020. (Best Demo/Poster Award)
  

Support

Please report any problems/bugs you face while installing and running AMYTISS to Abolfazl Lavaei or Mahmoud Khaled.

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

IMPaCT is an advanced open-source software tool for the parallelized verification and synthesis of large-scale stochastic systems using interval Markov chains (IMCs) and interval Markov decision processes (IMDPs), respectively. This tool serves to:

• construct IMCs and IMDPs as finite abstractions of underlying original complex systems;

• leverage interval iteration algorithms for formal verification and controller synthesis over infinite-horizon properties with convergence guarantees (in contrast to AMYTISS which exclusively handles finite-horizon specifications using finite MDPs).

IMPaCT is developed in modern ISO C++ and designed using AdaptiveCpp based on SYCL, a higher-level programming model that improves programming productivity on various hardware accelerators, for adaptive parallelism over CPUs and GPUs of all major 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.

Download

IMPaCT is an open-source tool and can be downloaded from its GitHub repository.

Tool paper

• B. Wooding and A. Lavaei, IMPaCT: Interval MDP Parallel Construction for Controller Synthesis of Large-Scale Stochastic Systems, submitted for publication, 2024.

• B. Wooding and A. Lavaei, IMPaCT: A Parallelized Software Tool for IMDP Construction and Controller Synthesis with Convergence Guarantees, 27th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2024), to appear, 2024.
  

Support

Please report any problems/bugs you face while installing and running IMPaCT to Abolfazl Lavaei or Ben Wooding.