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

该奖项的研究目标是建立一个随机的复杂系统的理论框架，这样，给定一个规格，我们可以分析系统，以确定规格将实现的概率，并自动找到一个输入法，以最大限度地提高这一概率。研究方法从现有的概率规范语言的适应性发展到适合于一般混合系统的形式，到创建满足给定概率规范的控制策略自动合成工具，最后到实现移动的机器人的自动部署工具。计算机程序或数字电路的有限模型针对诸如安全性之类的时间逻辑属性进行检查（即，不好的事情永远不会发生），活性（即，好的事情最终会发生），或者更丰富的规范。近年来，形式综合的对偶问题引起了人们越来越多的兴趣，其焦点是构造一个连续系统的控制器，使其通过设计是安全和正确的。这些努力集中在非随机系统。然而，现实世界中的系统，在随机输入和所有的传感器都受到噪声的影响，如果成功的话，这项研究的结果将导致通用的计算工具的分析和控制的随机系统的连续动态。这些技术的应用范围很广，从电网、个人和军事用途的自主机器人和生物医学设备等工程系统，到遗传网络等自然系统，乃至整个生态系统。这项研究与教育和推广计划密切相关，包括本科生课程的开发，本科生和高中生参与研究，以及PI参与波士顿大学的Upward Bound计划等推广活动。

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.