We introduce OmegaThreads, a tool for automatic synthesis of correct-by-construction controllers for control systems from ω-regular specifications. It accepts general nonlinear control systems from which discrete abstractions (a.k.a. symbolic models) are constructed. Specifications are provided directly as deterministic parity Automata (DPA) or as linear temporal logic (LTL) formulae. OmegaThreads constructs two-player parity games and searches for a winning strategies playing as a controller against the symbolic models. If found, OmegaThreads extracts the winning strategies as a Mealy machines.

Increasing levels of autonomy in safety-critical systems such as autonomous vehicles, airplanes, and medical robots, pose questions about their safety, thus compelling the scientific community to provide novel techniques for the design of foolproof safety-critical control software (SCCS). One promising approach for designing formally-correct SCCS is to use unambiguous formal descriptions for design requirements and, at the same time, automate the development and implementation processes. In this poster, we introduce OmegaThreads [3], a tool for automated synthesis of formally-correct controllers for control systems from ω-regular specifications.

Reachability analysis is a critical tool for the formal verification of dynamical systems and the synthesis of controllers for them. Due to their computational complexity, many reachability analysis methods are restricted to systems with relatively small dimensions. One significant reason for such limitation is that those approaches, and their implementations, are not designed to leverage parallelism. They use algorithms that are designed to run serially within one compute unit and they can not utilize widely-available high-performance computing (HPC) platforms such as many-core CPUs, GPUs and Cloud-computing services. This paper presents PIRK , a tool to efficiently compute reachable sets for general nonlinear systems of extremely high dimensions. PIRK can utilize HPC platforms for computing reachable sets for general high-dimensional non-linear systems. PIRK has been tested on several systems, with state dimensions up to 4 billion. The scalability of PIRK ’s parallel implementations is found to be highly favorable.

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.

Large-scale stochastic systems have recently received significant attentions due to their broad applications in various safety-critical systems such as traffic networks and self-driving cars. In this poster, we describe the software tool 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 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 a 7-dimensional nonlinear model of a BMW 320i car by synthesizing autonomous parking controllers.

The correctness of control software in many safety-critical applications such as autonomous vehicles is crucial. One technique to achieve correct control software is called "symbolic control", where complex systems are approximated by finite-state abstractions. Then, using those abstractions, provably-correct digital controllers are algorithmically synthesized for concrete systems, satisfying complex high-level requirements. Unfortunately, the complexity of synthesizing such controllers grows exponentially in the number of state variables. However, if distributed implementations are considered, high-performance computing platforms can be leveraged to mitigate the effects of the state-explosion problem.

The correctness of control software in many safety-critical applications such as autonomous vehicles is very crucial. One approach to achieve this goal is through “symbolic control”, where complex physical systems are approximated by finite-state abstractions. Then, using those abstractions, provably-correct digital controllers are algorithmically synthesized for concrete systems, satisfying some complex high-level requirements. Unfortunately, the complexity of constructing such abstractions and synthesizing their controllers grows exponentially in the number of state variables in the system. This limits its applicability to simple physical systems. This paper presents a unified approach that utilizes sparsity of the interconnection structure in dynamical systems for both construction of finite abstractions and synthesis of symbolic controllers. In addition, parallel algorithms are proposed to target high-performance computing (HPC) platforms and Cloud-computing services. The results show remarkable reductions in computation times. In particular, we demonstrate the effectiveness of the proposed approach on a 7-dimensional model of a BMW 320i car by designing a controller to keep the car in the travel lane unless it is blocked.

No abstract available.

This paper presents different multiprocessor implementations of the proportional-integral-derivative (PID) controller using two technologies: 1) field programmable gate array (FPGA)-based multiprocessor system-on-chip (MPSoC); and 2) multicore microcontrollers (MCUs). Techniques to implement a parallelized PID controller, a multi-PID controller, and a self-tuning PID controller are proposed. These techniques are verified using hardware (HW) in the loop (HIL) simulations. Then, the paper presents a detailed case study of an embedded real-time (RT) self-tuning PID controller for a 1-degree-of-freedom (1-DOF) aerodynamical system. This includes controller design, parameters tuning, and implementation using a multiprocessor system. Results proved the effectiveness of the proposed techniques to improve performance and functionality. It is shown that customizing HW and software (SW) within MPSoCs provides higher RT performance. Moreover, using multicore MCUs can reduce design time, implementation time, and cost, while keeping adequate performance. Therefore, it is possible to realize and implement complex RT embedded controllers that employ advanced control algorithms in rapid, effective, and cost-efficient fashion.