Verifying if a process controller achieves a desired goal regarding safety specifications or performance is an important task in practice. This work presents a method for controller verification and parametrization of uncertain polynomial discrete-time systems with closed-loop requirements. Apart from quantitative constraints, also qualitative requirements, which are not directly linked to a specific time or amplitude, are considered. For formalizing these constraints, we employ linear temporal logic formulas and polynomial inequalities. Uncertainties can be considered in the input, the output, the initial conditions and the model parameters to account e.g. for model plant mismatch and noise, described as unknown-but-bounded variables. We combine the requirements and the system dynamics into a nonlinear feasibility problem to verify the controller and determine admissible controller parametrization. This problem is solved by relaxing it to a mixed-integer linear program. The relaxation procedure guarantees that the derived set of possible parametrization fulfill the quantitative and qualitative requirements of the closed-loop behavior despite the present uncertainties. The proposed method is illustrated by verifying and parametrizing a controller for a two tank system.
