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.