IST Lunch Bunch

Tuesday October 4, 2011 12:00 PM

Automatic Verification of Region Stability of Hybrid Systems

Speaker: Sayan Mitra, Electrical & Computer Engineering, University of Illinois at Urbana-Champaign
Location: Annenberg 105
As motivation, consider a system consisting of several mobile robots which coordinate their behavior according to some protocol. We would like 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 coarseness in the abstraction itself. 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.
Series IST Lunch Bunch

Contact: Sydney Garstang at x2813 sydney@caltech.edu
For more information visit: http://www.cs.caltech.edu/seminars/lunch_bunch.html