IST Lunch Bunch

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.