"The Symbolic Approach to Hybrid Systems"

Dr. Thomas Henzinger, from UC Berkeley 

April 23, 2003 - 1:30 pm to 3:00 pm

2460 AV Williams Building

Tom Henzinger is a Professor of Electrical Engineering and Computer Sciences at the University of California, Berkeley.

He holds a Dipl.-Ing. degree in Computer Science from Kepler University in Linz, Austria, an M.S. degree in Computer and Information Sciences from the University of Delaware, and a Ph.D. degree in Computer Science from Stanford University (1991).
He was an Assistant Professor of Computer Science at Cornell University (1992-95), and a Director of the Max-Planck Institute for Computer Science in Saarbruecken, Germany (1999).

His research focuses on modern systems theory, especially formalisms and tools for the component-based and hierarchical design, implementation, and verification of embedded, real-time, and hybrid systems. His HyTech tool was the first model checker for mixed discrete-continuous systems.

ABSTRACT

A hybrid system is a dynamical system whose state has both a discrete component, which is updated in a sequence of steps, and a continuous component, which evolves over time. Hybrid systems are a useful modeling tool in a variety of situations, including control, robotics, circuits, biology, and finance.

We survey a computational approach to the design and analysis of hybrid systems which is based on the symbolic discretization of continuous state changes. On the theoretical side, we classify infinite, hybrid state spaces as to which finite, discrete abstractions they admit. This classification enables us to apply concepts and results from concurrency theory, model checking, and game theory to hybrid systems. On the practical side, we discuss several options for implementing the symbolic approach to hybrid systems, and point to existing tool support.