Symbolic Models and Control of Discrete-Time Piecewise Affine Systems: An Approximate Simulation Approach

Symbolic models have been recently used as a sound mathematical formalism for the formal verification and control design of purely continuous and hybrid systems. In this note we propose a sequence of symbolic models that approximates a discrete-time Piecewise Affine (PWA) system in the sense of approximate simulation and converges to the PWA system in the so-called simulation metric. Symbolic control design is then addressed with specifications expressed in terms of non-deterministic finite automata. A sequence of symbolic control strategies is derived which converges, in the sense of simulation metric, to the maximal controller solving the given specification on the PWA system.