1. Symbolic abstraction of a complex system

In this section, we present a general methodology for calculating a symbolic model of a dynamic system (Abstraction step 1 in figure 1 ). We then present the fundamental theorem of symbolic control, which certifies that the controllers synthesized on the basis of the symbolic model are "correct by construction" for the original system (Concretization step 3 in figure 1 ). The symbolic approach presented in this section is the result of a synthesis of numerous works in the literature. Those wishing to delve deeper into the mathematical aspects presented in this section may wish to start with the work of