Please reach me with any questions, apply by sending CV to my gmail account.
Best, Jacek Cyranka
Question we address: How to show that an autonomous vehicle (e.g. self-driving car) never collides with an obstacle?
Cyber-Physical systems denote various mechanizm that are controlled or monitored by computer algorithms The recent trend in CPS engineering autonomous cyber-physical systems (CPS) is to deploy a deep neural network (DNN) as a CPS controller. Some safety critical industrial applications include
The main concern about CPS development is the safety. Provably verifying safety properties of CPS is crucial for the engineering practice. Errors in CPS can lead to disastrous consequences, prominent examples include the Ariane 5 rocket crash in 1996. It is often crucial, especially when DNN controllers are in use, to demonstrate that for example an autonomous mobile never collides with obstacles on some given race track, or a spaceship reaches its destination and lands succesfully. Widely available computational power makes this question answerable using specialized computer algorithms. Such algorithms are blending together modern techniques from several areas of computer science and mathematics, including interval arithmetic, numerical analysis, differential equations and machine learning.
In this context I have led research on a scalable algorithm for verification of safety of DNN controlled CPS based on the concept of Lagrangian Reachability [1,2]. The current research is assuming that the mathematical model of CPS is given as differential equations. Definition of arbitrary complicated CPS, its controller, parameters and initial set are parsed from an input file. To verify e.g. safety property of the provided input system, the solution set starting at the provided initial state set must be bounded. Due to the model complexity and nonlinearity the solutions are not in closed form. Hence, the algorithm (LRT) to be sound must combine numerical methods and advanced algorithms. To guarantee conservativeness all numerical computations are performed using interval arithmetic.
Currently international research team involving researchers including UC San Diego, Texas Tech and TU Wien have been working on implementing scalable LRT algorithm in C++. Current efforts are on verifying that a simple neural circuit inspired by C-Elegans worm trained using reinforcement learning  is able to stabilize a cart-pole, perform parallel parking, and some related control tasks. One appealing design strategy for controllers is to use deep neural networks (DNNs). Safety properties of such controllers, however, remain largely unknown. I remark that this research falls into the topic of reliable/explainable AI, which is emerging as one of the most important problems in modern engineering.
Model free control based on Reinforcement Learning
Our current algorithm, although being state of the art assumes that the model is given as differential equations. Recent effort of engineering is however focused on model-free techniques where optimal control is performed by utilizing data input only, e.g. sensor readings or video camera input. Image input can be handled by using convolutional neural networks (CNNs).
As a future research, we will work on extending our techniques to the settings, where the exact model is not given / not known at all. It will require however establishing reliable reinforcement methods, e.g. policy gradient and safe AI in general. We will be utilizing major machine learning packages, and implement in Python.
 Jacek Cyranka, Md. Ariful Islam, Greg Byrne, Paul Jones, Scott A. Smolka, Radu Grosu, Lagrangian Reachability, CAV 2017  Jacek Cyranka, Md. Ariful Islam, Scott A. Smolka, Sicun Gao, Radu Grosu, Tight Continuous-Time Reachtubes for Lagrangian Reachability, IEEE CDC 2018  Mathias Lechner, Radu Grosu, Ramin M. Hasani, Worm-level Control through Search-based Reinforcement Learning, NIPS 2017Target conferences: