October 07, 2011, Webb 1100

As motivation, consider a system consisting of several mobile robots which coordinate their behavior according to some protocol. We would ike to automatically verify that even when some robots fail the remaining reach a desired configuration. This is an example of a liveness property called Region Stability. In this talk, we present an algorithm for verifying region stability of a general class of systems which can evolve both discretely and continuously (also called hybrid systems). Our algorithm iteratively abstracts and refines the discrete-continuous behavior of the hybrid automaton with hybrid-step relations. A non-well-founded relation may suggest a real counter-example to the region stability property, or it may correspond to a spurious counterexample arising from the a coarseness in the abstraction. Distinguishing these cases, our algorithm refines the abstraction appropriately. We show completeness of the algorithm for a restricted class of hybrid automata (initialized rectangular) and also discuss experimental results for more general linear hybrid automata where Lyapunov functions are used for constructing the abstract relations.

Sayan Mitra is an Assistant Professor of Electrical and Computer Engineering at the University of Illinois at Urbana-Champaign since 2008. His research interests are in verification of cyber-physical systems, distributed algorithms, and formal methods. Prior to joining Illinois, he was a post-doctoral fellow at the Center for Mathematics of Information of California Institute of Technology for a year and earned a Ph.D. from MIT in 2007. He received National Science Foundation's CAREER award and Air Force's Summer Faculty Fellowship award in 2011.