Reachability Analysis of Hybrid Systems

Goran Frehse / Persyval-Lab

Hybrid systems describe the evolution of a set of real-valued variables over time with ordinary differential equations and event-triggered resets. Set-based reachability analysis is a useful method to formally verify safety and bounded liveness properties of such systems. Starting from a given set of initial states, the successor states are computed iteratively until the entire reachable state space is exhausted. While reachability is undecidable in general and even one-step successor computations are hard to compute, recent progress in approximative set computations allows one to fine-tune the trade-off between computational cost and accuracy. In this talk we give an introduction to reachability analysis and present some of the techniques with which systems with complex dynamics and hundreds of variables have been successfully verified.
Bio:
Goran Frehse is an assistant professor of computer science at Verimag  Labs, University of Grenoble, France. He holds a Diploma in Electrical Engineering from Karlsruhe Institute of Technology, Germany, and a PhD in Computer Science from Radboud University Nijmegen, The Netherlands. He was a PostDoc at Carnegie Mellon University from 2003 to 2005. Goran Frehse developed PHAVer, a tool for verifying Linear Hybrid Automata, and is leading the ongoing development of SpaceEx, a verification platform for hybrid systems.