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

职业：基于稳健轨迹的随机混合系统抽象和验证分析

• 批准号: 0953976
• 负责人: Anak Agung Julius
• 金额: $ 53.68万
• 依托单位: Rensselaer Polytechnic Institute
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-02-01 至 2017-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0953976&HistoricalAwards=false
• 关键词: CAREER; Robust; Trajectory; Based; Analysis

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.

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