Symbolic control design of nonlinear systems with outputs

Formal methods have been recently used as the basis of a systematic framework to address control design of continuous or hybrid systems with specifications expressed in a logic form. However, results available in the literature assume full information of the state, or of its quantization. This information may not be available in relevant applications. In this paper, we consider the more realistic scenario where the controller cannot access the state of the plant but can only access a quantized measurement of its outputs where nonidealities of the sensing devices can be modeled. We focus on a control problem where the plant is described by a possibly unstable continuous-time nonlinear control system, the controller is dynamic, digital and quantized, and takes as input a (quantized) measurement of the output of the plant, and the specification is expressed in terms of regular languages. The solution to the control problem is based on formal methods. A finite-state system, also called symbolic model approximating the plant is first derived and then used to find the solution to the control problem. An illustrative example is provided and the symbolic control of a car-like robot is presented.