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.