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

混合系统（确定性和随机性）被广泛用作建模许多工程系统和自然现象的数学框架，从生物分子过程到现代空中交通管制系统。混合系统中最重要的分析问题之一是可达性/安全性分析，其中感兴趣的问题是系统是否可以在其执行过程中进入不期望的状态。对于随机混合系统，同样的问题是问一个概率限定符，即，这种事件发生的概率是多少。这个问题在分析工程系统的性能或正确性，以及自然现象（如细胞生物分子过程）的数学模型的准确性方面至关重要。该项目基于随机混合系统的执行轨迹或其抽象，开发可达性/安全性分析的形式化分析方法。在这项研究中使用的主要工具是轨迹鲁棒性的概念，这是建立使用互模拟功能。该技术提供了许多优于其他方法的优点，包括实现简单，更好的复杂性，易于并行实现，以及部分验证的可能性。该项目还旨在将分析从静态可达性/安全属性扩展到由时序逻辑指定的动态属性。研究计划包括开发必要的理论结果，算法和软件工具，用于基于轨迹的分析理论的应用。将理论成果集成到软件工具中将在工业界和学术界传播研究成果方面发挥重要作用。此外，该项目还在不断努力将研究成果应用于尖端工程挑战，例如使用细菌的微尺度驱动和便携式紫外线水消毒器的开发。与研究计划并行的是，该项目的教育议程涉及K-12，本科和研究生教育。教育计划的更广泛的影响是教育新的工程师和研究人员，他们精通多学科研究合作，并意识到这些活动的巨大潜力。教育计划的推广部分还将提高大学预科学生对工程和研究职业的潜力和吸引力的认识。

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.