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

Sponsor: National Science Foundation

Award Number: 0928776

Abstract:

The research objective of this award is to establish a theoretical framework for stochastic, complex systems
such that given a specification, we can analyze the system to determine the probability that the specification
will be achieved and automatically find an input law to maximize this probability. The research approach
progresses from the adaptation of existing probabilistic specification languages into a form suitable for a
general class of hybrid systems, to the creation of tools for the automatic synthesis of control strategies to
satisfy a given probabilistic specification, and finally to an implementation of those tools for the automatic
deployment of mobile robots.

In formal analysis, finite models of computer programs or digital circuits are checked against temporal
logic properties such as safety (i.e., something bad never happens), liveness (i.e., something good eventually
happens), or richer specifications. In recent years, there has been a growing interest in the dual problem of
formal synthesis, where the focus is to construct a control for a continuous system that is safe and correct
by design. These efforts have centered on non-stochastic systems. Real-world systems, however, invariably
evolve 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 and
control 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, and
biomedical devices, to natural systems such as genetic networks up to entire eco-systems. The research is
closely coupled to an educational and outreach plan, including curriculum development at the undergraduate
level, involvement of both undergraduate and high school students in the research, and participation of the
PIs in outreach events such as the Upward Bound program at Boston University.