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.