\textsf{AMYTISS}: parallelized automated controller synthesis for large-scale stochastic systems

DOI10.1007/978-3-030-53291-8_24zbMATH Open1481.93037arXiv2005.06191OpenAlexW3046763300MaRDI QIDQ2226754FDOQ2226754

Authors: Abolfazl Lavaei, Mahmoud Khaled, Sadegh Soudjani, Majid Zamani 

Publication date: 9 February 2021

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/2005.06191

Recommendations

• Towards scalable synthesis of stochastic control systems
• Compositional controller synthesis for stochastic games
• scientific article; zbMATH DE number 2163041
• Automata-based controller synthesis for stochastic systems: a game framework via approximate probabilistic relations
• Control design for specifications on stochastic hybrid systems

zbMATH Keywords

parallel algorithmsdiscrete-time stochastic systemsautomated controller synthesisfinite MDPshigh performance computing platform

Mathematics Subject Classification ID

Markov and semi-Markov decision processes (90C40) Large-scale systems (93A15) Synthesis problems (93B50) Discrete-time control/observation systems (93C55) Stochastic systems in control theory (general) (93E03) Software, source code, etc. for problems pertaining to systems and control theory (93-04)

Cited In (8)

• Automata-based controller synthesis for stochastic systems: a game framework via approximate probabilistic relations
• Formal abstraction and synthesis of parametric stochastic processes
• A learner-verifier framework for neural network controllers and certificates of stochastic systems
• Automated verification and synthesis of stochastic hybrid systems: a survey
• Similarity quantification for linear stochastic systems: a coupling compensator approach
• SySCoRe: Synthesis via Stochastic Coupling Relations
• AMYTISS
• Certified reinforcement learning with logic guidance

This page was built for publication: \textsf{AMYTISS}: parallelized automated controller synthesis for large-scale stochastic systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2226754)