CAREER: Robust Trajectory Based Analysis for Stochastic Hybrid Systems Abstraction and Verification

点击翻译按钮获取中文摘要

Hybrid systems (deterministic and stochastic) are widely used as the mathematical framework to model many engineering systems and natural phenomena, ranging from biomolecular processes to modern air traffic control systems. One of the most important analysis problems in hybrid systems is reachability/safety analysis, where the question of interest is whether the system can enter an undesirable state during its execution. For stochastic hybrid systems, the same question is asked with a probabilistic qualifier, i.e., what is the probability of the occurrence of such an event. This question is crucial in analyzing the performance or correctness of engineering systems, and the accuracy of the mathematical models of natural phenomena, such as cellular biomolecular processes. This project develops formal analysis methods for reachability/safety analysis based on the execution trajectories of stochastic hybrid systems or their abstraction. The main tool used in this research is the notion of trajectory robustness, which is established using bisimulation functions. This technique offers a number of advantages over other methods, including simplicity of implementation, better complexity, easiness of parallel implementation, and possibility of partial verification. The project also aims to extend the analysis from static reachability/safety properties to dynamic ones that are specified by temporal logic.The research program includes the development of necessary theoretical results, algorithms, and software tools for the application of the theory of trajectory based analysis. The integration of the theoretical results in a software tool will play an important role in disseminating the research output in the industry and academia. There are also ongoing efforts in applying the results in cutting edge engineering challenges, such as microscale actuation using bacteria and the development of portable UV-based water sterilizer.In parallel with the research program, this project has an educational agenda involving K-12, undergraduate and graduate level education. The broader impact of the educational program is in educating new engineers and researchers that are fluent in multidisciplinary research collaborations and are aware of the tremendous potentials of such activities. The outreach component of the educational program will also improve pre-college students' awareness of the potential and attractiveness of engineering and research careers.