AMYTISS: Parallel 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 such as autonomous driving. 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 (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: Parallel Automated Controller Synthesis for Large-Scale Stochastic Systems, 32nd International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science, Springer, 2020.

• 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 poster/demo award)

Support

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