Hierarchical synthesis of hybrid controllers from temporal logic specifications