On symbolic optimal control via approximate simulation relations

In the present paper we provide a methodology to approximately solve complex optimal control problems by using symbolic models. It has been shown in recent years that symbolic models (also called discrete abstractions) offer a convenient approach to deal with the analysis and control of complex qualitative control problems. We show how the notion of approximate simulation enables also the transfer of quantitative information between a given control system and its symbolic model. In particular, we show that quantities computed on the symbolic model provide lower and upper bounds for the optimal achievable cost of the control system. Finally, we indicate how the theoretical results may be applied to automatically synthesize controllers for qualitative specifications, given in a fragment of Linear Temporal Logics, and simultaneously guaranteeing some lower and upper bounds for the attainable cost.