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

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

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.