Optimal Control of Hybrid Systems using Formal Methods

Collaborators: Pavithra Prabhakar

Using formal methods to synthesize a controller for hybrid system emits a formally correct guarantee on the performance of the system. There are many areas where formal methods apply in solving controller synthesis problem. In this project, I developed an abstraction-refinement based algorithm to compute the optimal controller for a given discrete time switching system under regular objectives. The discrete time system is abstracted into a weighted two-player graph that conserves the cost properties of the system. Then, for each iteration of the algorithm, the abstraction of the system is refined, and the optimal strategy on the graph is computed. The strategy is guaranteed to produce suboptimal cost that converges to an optimal cost as the abstraction gets more refined.

The abstraction-refinement based approach is extended to synthesize an optimal controller with ω-regular objectives. This technique involves solving a mean-payoff game on a weighted parity graph given by the product of a Buchi automaton representing the regular objectives and a transition system representing the system dynamics.

This project started when I visited IMDEA Software Institute at Madrid over the summer of 2014.


  1. Y. P. Leong and P. Prabhakar, “Optimal control with regular objectives using an abstraction- refinement approach,” in American Controls Conf. (ACC), 2016, pp. 5161–5168.