Polytopic Trees for Verification and Control of Hybrid Systems

Hybrid systems demonstrate both continuous and discrete behaviors, making it computationally difficult to verify and control. We introduce "polytopic trees”, which is a novel, efficient representation for reachability properties. The central idea is to compute polytopic trajectories, which provide a set of parameterized polytope-to-polytope transitions. These parameters are computed using (mixed-integer) convex programs. In the higher level, these polytopes are grown backward from a user-defined goal region in a tree fashion, providing an infinite set of trajectories that reach the goal while satisfying all the system constraints. The remaining effort is making these polytopes cover the state-space as much as possible. These polytopic trajectories can be used to synthesize hybrid control policies or to verify controllers that may be characterized by hybrid phenomena such as rectifier linear units in neural networks. We provide illustrative examples on contact-based robot manipulative control as well as verification of systems controlled with machine learning components such as deep neural networks and decision trees.