State space grids for low complexity abstractions

We consider an automated, algorithmic controller synthesis framework for perturbed nonlinear control systems to enforce complex specifications, in which an auxiliary transition system, also known as abstraction or symbolic model, is used as a finite substitute of the original control system in the controller design process. We specifically focus on reducing the computational effort to obtain abstractions, which is the most expensive step in the approach. To this end, we derive a functional to estimate the size of the abstraction, specifically, the number of transitions, and prove that after a suitable transformation the functional becomes strongly convex. Thus, the minimization of the estimated size of the abstraction is an unconstrained strongly convex optimization problem, which is straightforward to solve using standard methods. This permits us to use this functional as a heuristic to determine certain grid parameters for the construction of abstractions. We illustrate the benefits of the newly developed heuristic for two numerical examples.