  We define robust abstractions for synthesizing provably correct and robust
controllers for (possibly infinite) uncertain transition systems. It is shown
that robust abstractions are sound in the sense that they preserve robust
satisfaction of linear-time properties. We then focus on discrete-time control
systems modelled by nonlinear difference equations with inputs and define
concrete robust abstractions for them. While most abstraction techniques in the
literature for nonlinear systems focus on constructing sound abstractions, we
present computational procedures for constructing both sound and approximately
complete robust abstractions for general nonlinear control systems without
stability assumptions. Such procedures are approximately complete in the sense
that, given a concrete discrete-time control system and an arbitrarily small
perturbation of this system, there exists a finite transition system that
robustly abstracts the concrete system and is abstracted by the slightly
perturbed system simultaneously. A direct consequence of this result is that
robust control synthesis for discrete-time nonlinear systems and linear-time
specifications is robustly decidable. More specifically, if there exists a
robust control strategy that realizes a given linear-time specification, we can
algorithmically construct a (potentially less) robust control strategy that
realizes the same specification. The theoretical results are illustrated with a
simple motion planning example.
