Class05

Compositional modeling and complexity reduction in the formal verification of purely discrete systems have resulted in a wealth of system relationships, including the established notions of language inclusion, simulation and bisimulation relations. System refinement and equivalence for purely discrete systems require observations to be identical. When discrete computing systems interact with the physical world, modeled by continuous or hybrid systems, exact refinement and equivalence are both restrictive and not robust. In this talk, I will present a framework of system approximation based on approximate language inclusion, simulation and bisimulation relations. We define a hierarchy of approximation pseudo-metrics for language inclusion, simulation, and bisimulation. The established exact notions are captured as zero sections of the pseudo-metrics. For continuous systems, whether discrete-time or continuous-time, we show how to compute the bisimulation metrics using Lyapunov-like relaxations. Finally, we illustrate how this approach gives rise to novel methods for simulation-based safety verification as well as notions of robust semantics for discrete temporal logic specifications.

George J. Pappas received the Ph.D. degree from the University of California at Berkeley in December, 1998. In 2000, he joined the University of Pennsylvania where he is currently an Associate Professor in the Department of Electrical and Systems Engineering. He also holds secondary appointments in the Departments of Computer and Information Sciences, and Mechanical Engineering and Applied Mechanics. He has published over 100 articles in the areas of hybrid systems, hierarchical control systems, distributed control systems, nonlinear control systems, and geometric control theory, with applications to flight management systems, robotics, and unmanned aerial vehicles.

Dr. Pappas is the recipient of a National Science Foundation (NSF) Career Award in 2002, as well as the 2002 NSF Presidential Early Career Award for Scientists and Engineers (PECASE). He received the 1999 Eliahu Jury Award for Excellence in Systems Research from the Department of Electrical Engineering and Computer Sciences, University of California at Berkeley. His and his student’s papers were finalists for the Best Student Paper Award at the 1998 IEEE Conference on Decision and Control, the 2001 American Control Conference, the 2001 IEEE Conference on Decision and Control, the 2004 American Control Conference, and the 2004 IEEE Conference on Decision and Control. He is currently an Associate Editor for the IEEE TRANSACTIONS ON AUTOMATIC CONTROL.

Host: Prof. Cassandras
Student Host: James Kang