Verification of Control Laws Using Formal Methods

Add to your list(s) Download to your calendar using vCal

• Kestutis Siaulys, University of Cambridge
• Thursday 11 May 2017, 14:00-15:00
• Cambridge University Engineering Department, LR6.

If you have a question about this talk, please contact Tim Hughes.

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.

This talk is part of the CUED Control Group Seminars series.

This talk is included in these lists:

• Cambridge University Engineering Department, LR6
• All Talks (aka the CURE list)
• CUED Control Group Seminars
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge University Engineering Department Talks
• Cambridge talks
• Centre for Smart Infrastructure & Construction
• Chris Davis' list
• Computational Continuum Mechanics Group Seminars
• Featured lists
• Information Engineering Division seminar list
• Interested Talks
• School of Technology
• Signal Processing and Communications Lab Seminars
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• rp587

Note that ex-directory lists are not shown.