Formal design method of optimal controllers for hybrid systems with integrated qualitative/quantitative performance