  In this paper, we propose an approach to reduce the optimal controller
synthesis problem of hybrid systems to quantifier elimination; furthermore, we
also show how to combine quantifier elimination with numerical computation in
order to make it more scalable but at the same time, keep arising errors due to
discretization manageable and within bounds. A major advantage of our approach
is not only that it avoids errors due to numerical computation, but it also
gives a better optimal controller. In order to illustrate our approach, we use
the real industrial example of an oil pump provided by the German company HYDAC
within the European project Quasimodo as a case study throughout this paper,
and show that our method improves (up to 7.5%) the results reported in [3]
based on game theory and model checking.
