CAREER: Computational Methods for the Analysis and Design of Stochastic Hybrid Systems

信息和微尺度技术的最新进展使新一代嵌入式系统成为可能，从汽车和飞机到制造工厂，这些系统正在我们的日常生活中无处不在。这类应用由紧密耦合的物理和计算过程组成，这些过程在存在不确定性和可变性的情况下与环境动态交互。该项目旨在开发一个随机混合系统框架，为分析和设计这些系统提供理论、计算方法和软件工具。随机混合系统用局部一致马尔可夫决策过程逼近，该决策过程保持了局部均值和协方差。该项目解决了以下关键的研究挑战：(1)使用概率时间逻辑表达的系统属性的形式化分析。随机双模拟被用来提供近似马尔可夫过程的等效最小模型，并允许可扩展算法的发展。(2)采用随机最优控制设计高度自治的嵌入式控制系统。有效的算法是通过利用随机双模拟来设计的，这些随机双模拟考虑了可用的控制。采用基于模型的软件设计构建了一套支持工具，并进行了实验研究来验证结果。通过一系列现实挑战问题，将研究成果整合到本科和研究生课程中。技术成果、软件工具和教育材料将以电子方式提供，采用开放源码模式，并通过出版物和参加会议提供。该项目的更广泛目标是建立坚实的理论基础和计算方法，这些理论基础和计算方法将影响应用中的嵌入式系统设计，例如用于国土安全和环境监测的移动传感器网络、智能交通系统、机电系统和制造业中的化学过程。

Recent advances in information and micro-scale technologies are enabling a new generation of embedded systems that are pervading our daily lives, from automobiles and aircrafts to manufacturing plants. Such applications consist of tightly coupled physical and computational processes that dynamically interact with the environment in the presence of uncertainty and variability. This project aims at developing a stochastic hybrid system framework that provides the theories, computational methods, and software tools for analysis and design of such systems. Stochastic hybrid systems are approximated by locally consistent Markov decision processes that preserve local mean and covariance. The project addresses the following critical research challenges: (1) Formal analysis of system properties expressed using probabilistic temporal logics. Stochastic bisimulations are employed to provide equivalent minimal models of the approximating Markov processes and allow the development of scalable algorithms. (2) Design of embedded control systems with high degree of autonomy using stochastic optimal control. Efficient algorithms are designed by utilizing stochastic bisimulations that account for the available controls. Model-based software design is used for building a suite of supporting tools and experimental research is conducted to validate the results. The research advancements are integrated into the undergraduate and graduate curriculum using a series of realistic challenge problems. Technical results, software tools, and the education materials will be made available electronically using an open-source model as well as through publications and conference participation. The broader goal of the project is to establish solid theoretical foundations and computational methods that will impact embedded system design in applications such as mobile sensor networks for homeland security and environmental monitoring, intelligent transportation systems, and electromechanical systems and chemical processes in manufacturing.