  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.
