COCO: Control Equivalence for Cyber-Physical Models

Nonlinear differential equations are of paramount importance in the modeling of biochemical, epidemiological, cyber-physical and dependable systems. Unfortunately, their precise parameterization is often not possible due to finite-precision measurements or lack of information. Hence, in order to ensure safety in the presence of parameters that are subject to uncertainty, it thus becomes necessary to formally approximate the underlying dynamical system. A possible example may be, for instance, the task of verifying that the autopilot keeps the airplane in stable flight in the presence of realistic turbulence. Apart from safety verification, one may need to verify that the forecast underlying a dynamical system is not dramatically affected if model parameters are subject to fluctuations. A possible example may be the weather forecast, for instance. Despite the fact that the computation of tight formal approximations received a lot of attention in the last decades, it remains computationally demanding in the case of nonlinear dynamics. A universal approach for the simplification of difficult problems is that of model reduction where the idea is to formally relate the original problem to a smaller one which can be solved more efficiently. While model reduction techniques have been applied in the context of approximation problems in the past, no efficient reduction algorithms are available in the case of nonlinear dynamics. The project will close this gap by interpreting formal approximation problems as optimal control problems. The key novelty will be to identify symmetric dynamical systems by an efficient algorithm and to show that symmetric dynamics lead to symmetric control problems which can be reduced efficiently. Realistic nonlinear models of cyber-physical, biochemical and dependable systems that cannot be estimated by the current techniques due to their large size will be formally approximated. The results of the project will be made available to a broad audience via a software tool.

Nonlinear models are of paramount importance in the modeling of biochemical, epidemiological, cyber-physical and dependable systems. Unfortunately, their precise parameterization is often not possible due to finite-precision measurements or lack of information. Hence, in order to ensure safety in the presence of parameters that are subject to uncertainty, it thus becomes necessary to formally approximate the underlying dynamical system. Despite the fact that the computation of tight formal approximations received a lot of attention in the last decades, it remains computationally demanding in the case of nonlinear dynamics. A universal approach for the simplification of difficult problems is that of model reduction where the idea is to formally relate the original problem to a smaller one which can be solved more efficiently. While model reduction techniques have been applied in the context of approximation problems in the past, no efficient reduction algorithms are available in the case of nonlinear dynamics. The project initiated the journey towards efficient verification preserving reduction techniques but was terminated prematurely because the PI was offered, not least thanks to the Meitner project, a permanent position as an Associate Professor at Aalborg University, Denmark. First preliminary results paving the way to project's vision have been published however.