Abstract

In this talk, we show how general analysis/synthesis problems in control theory can be expressed as quantified first order formulas and introduce a verification approach based on formal methods (in particular, quantifier elimination (QE) algorithms). This verification approach works by expressing a verification criterion of choice in a mathematical form that one of the QE algorithms (such as cylindrical algebraic decomposition (CAD) or Weispfenning’s virtual substitution algorithm) are capable of checking.

Consequently, this allows us to analyse problems from a different angle. One of the main benefits of the proposed approach based on QE algorithms is that these procedures work by algebraically manipulating the mathematical expression representing the verification criterion to arrive at the conclusion and do not involve numerical techniques such as simulation or gridding. This guarantees that verification by QE algorithms does not miss a critical frequency or parameter combination at which the desired property is violated. Additionally, the generality of these methods allows us to relax some standard conditions like convexity of the cost function in the optimisation problem.

The downside to this approach is the computational penalty that has to be paid when compared to numerical methods, especially when a general QE algorithm (like CAD ) is used. Hence, we focus our attention to control problems that can be converted to quantifier elimination ones with a particular quantification structure.

As an example, we propose a method based on Weispfenning’s `quantifier elimination by virtual substitution’ algorithm for obtaining explicit model predictive control (MPC) laws for linear time invariant systems with quadratic objective and polytopic constraints. Weispfenning’s algorithm is applicable to first order formulas in which quantified variables appear at most quadratically. It has much better practical computational complexity than general quantifier elimination algorithms, such as cylindrical algebraic decomposition. Additionally, we show how this explicit MPC solution, together with Weispfenning’s algorithm, can be used to check recursive feasibility of the system, for both nominal and disturbed systems. Finally, we show how the structured singular value calculation problem can be tackled with Weispfenning’s algorithm as well.