Polytopic Trees for Verification and Control of Hybrid Systems

Wednesday, April 3, 2019 - 3:00pm to 3:30pm

Event Calendar Category

LIDS & Stats Tea

Speaker Name

Sadra Sadraddini



Building and Room Number

LIDS Lounge


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.


Sadra Sadraddini is a postdoctoral associate in Robot Locomotion Group in MIT CSAIL. He got his PhD in mechanical engineering in 2018 from Boston University, Boston, MA, and his bachelors in the same major from Sharif University of Technology in 2013. His research is focused on bridging the gap between formal methods and control theory, with a particular focus on verification and control of hybrid systems. Applications include robotics and transportation networks.