CSR--EHS: Collaborative Research: Verification of Probabilistic Hybrid Systems: Stability and Beyond

CSR--EHS：协作研究：概率混合系统的验证：稳定性及其他

• 批准号: 0614414
• 负责人: Nancy Lynch
• 金额: $ 23万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2006
• 资助国家: 美国
• 起止时间: 2006-08-01 至 2009-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0614414&HistoricalAwards=false
• 关键词: CSR; EHS; Collaborative; Research; Verification

Abstract:This collaborative project studies dynamical systems characterized by a combination of hybrid and probabilistic behavior. Hybrid behavior is characterized by discrete switching between system modes and continuous evolution within a mode. Such systems frequently arise in a wide range of applications, from power electronics and communication networks to economics and biology. In this research, a new modeling framework for such systems is developed, which supports external variables, compositional reasoning, and nondeterministic as well as probabilistic transitions. New stability criteria for such probabilistic hybrid systems are obtained. In contrast with existing results, they are formulated in terms of two independent components: a family of Lyapunov functions (one for each continuous mode) and a slow-switching condition of an average-dwell-time type. This modularity has the benefit of decoupling the search for Lyapunov functions from the verification of the desired properties of the discrete dynamics. The latter task is the focus of the project, and is treated using two complementary methods: one based on proving an invariant property, and another based on solving an optimization problem. These theoretical results are supported by development of new software tools.

翻译后摘要：这个合作项目研究动力系统的混合动力和概率行为的结合。混合行为的特征在于系统模式之间的离散切换和模式内的连续演化。 这种系统经常出现在广泛的应用中，从电力电子和通信网络到经济和生物学。在这项研究中，开发了一个新的建模框架，这样的系统，它支持外部变量，组合推理，以及不确定性和概率转换。新的稳定性准则，这样的概率混合系统。与现有的结果相比，他们制定的两个独立的组成部分：一个家庭的李雅普诺夫函数（一个为每个连续模式）和一个平均停留时间类型的慢开关条件。这种模块化的好处是解耦的搜索李雅普诺夫函数从所需的离散动态特性的验证。后一项任务是该项目的重点，并使用两种互补的方法进行处理：一种是基于证明不变属性，另一种是基于解决优化问题。新的软件工具的开发支持这些理论结果。