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.

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