AMYTISS swMATH ID: 36936 Software Authors: Lavaei, Abolfazl; Khaled, Mahmoud; Soudjani, Sadegh; Zamani, Majid Description: AMYTISS: a parallelized tool on automated controller synthesis for large-scale stochastic systems. In this paper, we propose a software tool, called AMYTISS, implemented in C++/OpenCL, for designing correct-by-construction controllers for large-scale discrete-time stochastic systems. This tool is employed to (i) build finite Markov decision processes (MDPs) as finite abstractions of given original systems, and (ii) synthesize controllers for the constructed finite MDPs satisfying bounded-time high-level properties including safety, reachability and reach-avoid specifications. In AMYTISS, scalable parallel algorithms are designed such that they support the parallel execution within CPUs, GPUs and hardware accelerators (HWAs). Unlike all existing tools for stochastic systems, AMYTISS can utilize high-performance computing (HPC) platforms and cloud-computing services to mitigate the effects of the state-explosion problem, which is always present in analyzing large-scale stochastic systems. We benchmark AMYTISS against the most recent tools in the literature using several physical case studies including robot examples, room temperature and road traffic networks. We also apply our algorithms to a 3-dimensional autonomous vehicle and 7-dimensional nonlinear model of a BMW 320i car by synthesizing an autonomous parking controller. Homepage: https://arxiv.org/abs/2005.06191 Keywords: automated controller synthesis; discrete-time stochastic systems; high performance computing platform; parallel algorithms Related Software: FAUST2; StocHy; SReach; ProbReach; PRISM; SCOTS; Modelica; Sostools; ToolboxLS; z3; SeDuMi; pFaces; SReachTools; GitHub; MoDeST; Storm Cited in: 5 Publications Standard Articles 2 Publications describing the Software, including 2 Publications in zbMATH Year AMYTISS: parallelized automated controller synthesis for large-scale stochastic systems. Zbl 1481.93037Lavaei, Abolfazl; Khaled, Mahmoud; Soudjani, Sadegh; Zamani, Majid 2020 AMYTISS: a parallelized tool on automated controller synthesis for large-scale stochastic systems. Zbl 07300872Lavaei, Abolfazl; Khaled, Mahmoud; Soudjani, Sadegh; Zamani, Majid 2020 all top 5 Cited by 8 Authors 4 Lavaei, Abolfazl 4 Zamani, Majid 3 Soudjani, Sadegh 2 Abate, Alessandro 2 Khaled, Mahmoud 1 Caccamo, Marco 1 Peruffo, Andrea 1 Zhong, Bingzhuo Cited in 1 Serial 2 Automatica Cited in 4 Fields 4 Systems theory; control (93-XX) 3 Computer science (68-XX) 2 Operations research, mathematical programming (90-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year