Finite abstractions with robustness margins for temporal logic-based control synthesis

This paper introduces a notion of finite abstractions that can be used to synthesize robust controllers for dynamical systems from temporal logic specifications. These finite abstractions, equipped with certain robustness margins, provide a unified approach to various issues commonly encountered in implementing control systems, such as inter-sample behaviors of a sampled-data system, effects of imperfect state measurements and unmodeled dynamics. The main results of this paper demonstrate that the robustness margins can effectively account for the mismatches between a control system and its finite abstractions used for control synthesis. The quantitative nature of the robustness margins also makes it possible to study the trade-offs between the performance of controllers and their robustness against various types of adversaries (e.g., delays, measurement errors, or modeling uncertainties). We use a simple adaptive cruise control (ACC) example to illustrate such robustness-performance trade-offs.