Approximately bisimilar discrete abstractions of nonlinear systems using variable-resolution quantizers

This paper presents a method for the design of discrete abstract models of nonlinear continuous-state systems under the framework of approximate bisimulation. First, the notion of quantizer embedding, which transforms a continuous-state system into a finite-state system, is extended to a variable-resolution setting. Next, it is shown that the series of conditions for approximate bisimulation can be converted into a set of linear inequalities, which can be verified by a linear programming solver. From this result, we obtain an algorithm that repeatedly refines a variable-resolution mesh until approximate bisimulation with a prescribed error specification is achieved.