Reachability analysis is a process of computing the set of states that a system can reach from an initial region. A system is safe when the set of its reachable states does not intersect with the unsafe region in the state-space. Thus, reachability analysis has become an essential technique for ensuring the safety of emerging systems like CPSs. However, computing the reachable states of CPSs is a very difficult problem, as these systems are most often nonlinear, and their state-space is uncountably infinite.
(a) Discrete reachtube computation (b) Continuous reachtube computation (c) Reducing wrapping effect
While most existing techniques use Taylor-expansion in time, variational-expansion in space or combination of both, we have worked on proposing an alternative (and orthogonal) technique for computing a conservative reachtube using Lagrangian description of finite strain theory . By computing a stretching factor that is derived from an over-approximation of the gradient of the solution-flows, we have developed techniques for computing a conservative reachtube. One critical challenge in computing conservative reachtube is reducing the so called wrapping effect. This occurs when a set of states is wrapped within a box defined in a particular norm. Our technique reduces the wrapping effect by computing optimal weighted norm analytically. By applying our technique on multiple benchmark problems, we have illustrated that it computes tighter reachtubes in most benchmark problems compared to the well-established tools. This tighter bound on reachtubes reduces false-positive in safety verifications and makes our technique more appealing in the verification of CPSs.
(a) Discrete reachset (b) Continuous reachset
Scalable Reachability Analysis:
Reachability analysis has been proved to be useful in verifying safety properties of CPS. However, existing tools are not scalable enough to verify large scale CPSs. Currently, I am working on developing a reachability tool to address this scalability issue. This newly developed tool will able to verify safety property of diverse class of large scale CPS, including, automated vehicles, surgical robots, collaborative human-robot manufacturing, smart grids and deep neural networks.
Verifying Deep Neural Networks:
Recent advances of deep neural network (DNN) in solving diverse challenging tasks have inspired system developers to use DNN in safety-critical CPSs such automated car and air-traffic collusion avoidance systems. However, incidents like Uber and Tesla crashes, have emphasized a need for verifying the systems that uses DNN-based controllers. Due to the nonlinear physical dynamics of CPSs, existing techniques are not sufficient to verify DNN when used as a controller for CPSs. Currently, I am working on developing a new method for safety verification of DNN-based CPSs using reachability analysis.
 J. Cyranka*, M. A. Islam*, S. Smolka, and R. Grosu. Tight continuous-time reachtubes for lagrangian reachabililty. In International Conference on Decision and Control (CDC), 2018. [*equal contribution] (to appear).
 J. Cyranka*, M. A. Islam*, S. Smolka, and R. Grosu. Lagrangian reachabililty. In
International Conference on Computer Aided Verification (CAV), 2017. [*equal contribution].