Human Centered Synthesis of Provably Correct Controllers for Hybrid Systems

(NSF CNS 1218109)

Hybrid systems are a mathematical framework that has been widely used to model engineering and natural systems whose dynamics have both continuous and discrete aspects. Applications range from modern "fly-by-wire" airplanes to cellular biology. A controller for a hybrid system observes the execution of the system and issues input signals and/or trigger events in the hybrid system so as to meet the system's goals and safety requirements. An outstanding problem is that for complex hybrid systems existing methods for controller synthesis require exceedingly large computational resources.

This project seeks to address the high computational demands of constructing controllers for hybrid systems in a new way. The novelty of the approach lies in using human-centered computing (crowdsourcing), while ensuring that the obtained controller is correct. The expected outcomes of this project are mathematical theory and algorithms that will enable the idea above for a wide range of problems, including those involving nonlinear systems and random events. These results are further implemented in simulator computer games, which will be deployed online. The amount of computing resource that can be potentially be harvested through crowdsourcing is very high. Earlier crowdsourcing applications such as reCAPTCHA, FoldIt, and Wikipedia have recorded billions of hours of effort by their human contributors. Beyond solving the controller synthesis problem, the outcomes of this project can lead to new ways to tap into this resource for solving new problems.

As a testbed, we have developed an online computer game that models the dynamics of an inverted pendulum (click here). With this online game, we will collect trajectories generated by human players and use them to synthesize a controller for an actual inverted pendulum plant.

Project personnel
Dr. Agung Julius (PI)
Sayan Saha (Grad. Student)
Andrew Winn (Grad. Student)
Christopher Fry (Undergraduate researcher)
Bilal Salam (Undergraduate researcher)
Christopher Hladic (former Grad. Student)
Andrew Hanson (former Grad. Student)

Publications

A.K. Winn, A.A. Julius, "Feedback Control Law Generation for Safety Controller Synthesis", in Proc. IEEE Conf. Decision and Control, Firenze, Italy, 2013.
H. Abbas, A. Winn, G. Fainekos, A.A. Julius, "Functional Gradient Descent Method for Metric Temporal Logic Specifications", in Proc. American Control Conference, Portland, OR, 2014. "
S. Saha, A.A. Julius, "Trajectory-Based Formal Controller Synthesis for Multi-Link Robots", in Proc. IEEE Conf. Decision and Control, Los Angeles, CA, 2014.
A.K. Winn, A.A. Julius, "Safety Controller Synthesis Using Human Generated Trajectories", accepted for publication in IEEE Trans. Automatic Control, 2014.

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.