DynSyst_Special_Topics: A formal approach to the control of stochastic dynamic systems

该奖项的研究目标是为随机、复杂的系统建立一个理论框架，以便在给定规范的情况下，我们可以分析系统以确定实现该规范的概率，并自动找到使该概率最大化的输入法则。在形式分析中，计算机程序或数字电路的有限模型被检查与诸如安全性(即，坏的事情从未发生)、活性(即，好的事情最终发生)或更丰富的规格说明等时序逻辑特性。近年来，形式综合的对偶问题引起了人们越来越大的兴趣，其中的焦点是为一个连续系统构造一个安全且通过设计正确的控制。这些努力主要集中在非随机系统上。然而，真实世界的系统总是在随机输入下演化的，并且所有的传感器都受到噪声的影响。如果成功，本研究的结果将导致通用的计算工具来分析和控制具有连续动态的随机系统。这类技术的应用范围很广，从电网等工程系统、个人和军事用途的自主机器人以及生物医学设备，到遗传网络等自然系统，再到整个生态系统。这项研究与教育和外展计划密切相关，包括本科生和高中生参与研究的课程开发，以及个人投资机构参与外展活动，如波士顿大学的向上跳跃计划。

The research objective of this award is to establish a theoretical framework for stochastic, complex systemssuch that given a specification, we can analyze the system to determine the probability that the specificationwill be achieved and automatically find an input law to maximize this probability. The research approachprogresses from the adaptation of existing probabilistic specification languages into a form suitable for ageneral class of hybrid systems, to the creation of tools for the automatic synthesis of control strategies tosatisfy a given probabilistic specification, and finally to an implementation of those tools for the automaticdeployment of mobile robots.In formal analysis, finite models of computer programs or digital circuits are checked against temporallogic properties such as safety (i.e., something bad never happens), liveness (i.e., something good eventuallyhappens), or richer specifications. In recent years, there has been a growing interest in the dual problem offormal synthesis, where the focus is to construct a control for a continuous system that is safe and correctby design. These efforts have centered on non-stochastic systems. Real-world systems, however, invariablyevolve under stochastic inputs and all sensors are subject to noise.If successful, the results of this research will result in general-use computational tools for the analysis andcontrol of stochastic systems with continuous dynamics. Applications of such techniques are wide-spread,ranging from engineered systems such as power grids, autonomous robots for personal and military use, andbiomedical devices, to natural systems such as genetic networks up to entire eco-systems. The research isclosely coupled to an educational and outreach plan, including curriculum development at the undergraduatelevel, involvement of both undergraduate and high school students in the research, and participation of thePIs in outreach events such as the Upward Bound program at Boston University.