Path-oriented reachability verification of a class of nonlinear hybrid automata using convex programming. (English)
Barthe, Gilles (ed.) et al., Verification, model checking, and abstract interpretation. 11th international conference, VMCAI 2010, Madrid, Spain, January 17‒19, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-11318-5/pbk). Lecture Notes in Computer Science 5944, 78-94 (2010).
Summary: Hybrid automata are well-studied formal models for dynamical systems. However, the analysis of hybrid automata is extremely difficult, and even state-of-the-art tools can only analyze systems with few continuous variables and simple dynamics. Because the reachability problem for general hybrid automata is undecidable, we give a path-oriented reachability analysis procedure for a class of nonlinear hybrid automata called convex hybrid automata. Our approach encodes the reachability problem along a path of a convex hybrid automaton as a convex feasibility problem, which can be efficiently solved by off-the-shelf convex solvers, such as CVX. Our path-oriented reachability verification approach can be applied in the frameworks of bounded model checking and counterexample-guided abstraction refinement with the goal of achieving significant performance improvement for this subclass of hybrid automata.