Abstract:Hybrid automata are well studied formal models for analyzing hybrid systems - systems with both discrete and continuous components. Linear hybrid automata are a very important subclass of hybrid automata that can approximate nonlinear hybrid systems and serve as algorithmically analyzable models for these hybrid systems. The verification of linear hybrid automata is an interesting and challenging problem. In this talk, we will explore recent results in the application of counterexample guided abstraction refinement (CEGAR) to the analysis of linear hybrid automata. We will advocate the use of multiple abstractions for proving reachability properties, and present experimental evidence that demonstrates the success of this technique in solving benchmark problems. We will also survey directions for possible future work.

Sumit Kumar Jha is a PhD student with the Computer Science Department at Carnegie Mellon University. His main research interests are model checking, verification, systems biology and hybrid dynamical systems. In the past, Sumit has worked on the verification of hardware designs with the Intel India Undergraduate Research Program, the ab-initio prediction of protein structures with the MODBIO group at INRIA, the diagnosis of faults in discrete event systems using model checking at General Motors R&D, and the verification of ESQL (Extended Structured Query Language) queries in databases at Microsoft Research, Bangalore. Appointments: dcm@cs.cmu.edu