Abstract: In this talk we will consider a correctness property for hybrid systems called region stability, and methods for verifying that a given hybrid system satisfies this correctness property.

Classical notions of stability refer to a single equilibrium point, and have been intensively studied by both computer scientists and control theorists. But stability with respect to a single point does not seem to be always adequate to express the correctness property of a hybrid system. If we consider a heating system, where the temperature is specified by upper and lower bounds, such an equilibrium point does not even exist.

I will introduce a new notion of stability that refers to a region instead of an equilibrium point. For some cases of hybrid systems this gives the appropriate formalization of their correctness. I will situate our notion in the landscape of related properties in control theory and model checking.

Furthermore I will give a method for verifying region stability of hybrid systems, and I will present a tool that we have applied to solve a number of verification problems. Before, such verification problems have been out of reach for automatic methods.

From 1998 - 2003, Silke Wagner studied mathematics and computer science at the University of Saarland. She received a master's degree /(Diploma) /in mathematics with a thesis on "Extrapolation methods for the diffusion equation". In 2003 she became a Ph.D. Student at the Max Planck Institute for computer science in Saarbrücken where she was working in the Programming Logics Group, supervised by Prof. Andreas Podelski. She wrote her Ph.D. thesis on "Stability Proofs for Hybrid Systems". Since January 2008 Silke has been a Postdoctoral Fellow at CMU where she is collaborating with Prof. Edmund Clarke. Appointments: dcm@cs.cmu.edu