论文标题
Amytiss：大规模随机系统的并行自动化控制器合成
AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems
论文作者
论文摘要
在本文中，我们提出了一个称为Amytiss的软件工具，该工具在C ++/OpenCL中实现，用于设计针对大型离散时间随机系统的正确构造控制器。该工具用于（i）构建有限的马尔可夫决策过程（MDP）作为给定原始系统的有限抽象，以及（ii）为满足有限的高级高级属性（包括安全性，可及性，可触及到达范围的规格）合成构造有限的MDP的控制器。在Amytiss中，设计可扩展的并行算法使其支持CPU，GPU和硬件加速器（HWAS）中的并行执行。与所有现有的随机系统工具不同，Amytiss可以利用高性能计算（HPC）平台和云计算服务来减轻状态探索问题的影响，该问题始终存在于分析大型随机系统中。我们使用几个物理案例研究（包括机器人示例，室温和道路交通网络）对文献中最新工具进行了基准对抗文献中的最新工具。我们还将算法应用于3维自动驾驶汽车和7维非线性模型的BMW 320I汽车，通过合成自主停车控制器。
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.
