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.
The overarching goal of this project was to create techniques for ensuring that systems that are subject to both input and measurement noise behave in a desired manner. While inspired by problems in mobile robotics, the focus was on developing schemes based on the underlying mathematical models so that the results could be generally applicable. The desired behavior of the system was described through the use of temporal logics with the stochastic nature of the problem included by using the probabilistic variants. Schemes were developed to abstract a more standard model of a system, namely a set of differential equations, into a discrete model more amenable to the temporal logics used. These abstractions by design accounted for the uncertainty in the original system. The desired behavior of the system was described using a specification given in the temporal logic; these can be thought of as tasks. The robotic scenario provides intuitive examples such as Maximize the probability of moving between a set of desired locations while avoiding others. If a particular situation is encountered, then instead move to a third region. Algorithms were then derived and analyzed that found policies, that is a choice of actions to be applied, so as to at least approximately maximize the probability of accurately performing the given task. The project also produced similar algorithms that allowed for uncertainty or even complete lack of knowledge about different aspects of the environment. In the robotic scenario, for example, this could mean a disaster scenario where it is known there are survivors in the building but neither the layout of the building nor the locations of the survivors are known exactly.
