Specification, Design and Verification of Distributed Embedded Systems
Prof. Richard M. Murray
Thursday, December 9, 2010
|Abstract: We are investigating the specification, design, and verification of distributed systems that combine
communications, computation, and control in dynamic, uncertain, and adversarial environments.
Our goal is to develop methods and tools for designing control policies, specifying the properties of
the resulting distributed embedded system and the physical environment, and proving that the
specifications are met. In the area of hybrid systems, we have developed tools for analysis of
periodically controlled hybrid automata (PCHAs) that allow us to prove stability for control systems
that have slightly asynchronous controller execution (with bounds on the controller execution
period). We have also developed a promising set of results in receding horizon temporal logic
planning that allows automatic synthesis of complex dynamical systems, which are guaranteed, by
construction, to satisfy the desired properties even in the presence of adversary. The desired
properties are expressed in the language of temporal logic and the resulting system consists of a
discrete planner that plans, in the abstracted discrete domain, a set of transitions of the system to
ensure the correct behaviors and a continuous controller that continuously implements the plan.
|Bio: Richard M. Murray received the B.S. degree in Electrical Engineering from California Institute of
Technology in 1985 and the M.S. and Ph.D. degrees in Electrical Engineering and Computer
Sciences from the University of California, Berkeley, in 1988 and 1991, respectively. He is
currently the Thomas E. and Doris Everhart Professor of Control & Dynamical Systems and
Bioengineering at Caltech. Murray’s research is in the application of feedback and control to
networked systems, with applications in biology and autonomy. Current projects include
verification and validation of distributed embedded systems, analysis of insect flight control
systems, and biological circuit design.