COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > CUED Control Group Seminars > Verification of Control Laws Using Formal Methods

## Verification of Control Laws Using Formal MethodsAdd 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 Big Data
- Cambridge University Engineering Department Talks
- Centre for Smart Infrastructure & Construction
- Featured lists
- Information Engineering Division seminar list
- School of Technology
- Signal Processing and Communications Lab Seminars
- ndk22's list
- rp587
Note that ex-directory lists are not shown. |
## Other listsCambridge Institute for Sustainability Leadership Cambridge Energy Conference Cancer Research UK Cambridge Institute (CRUK CI) Seminars in Cancer## Other talksBuilt environment and violent crime: An environmental audit approach using Google Street View Prevalence of Meningococcal Carriage by Age in the African Meningitis Belt Repeated Measures and Mixed Model ANOVA Lightweight verification of separate compilation Curatorsâ€™ introduction to Codebreakers and Groundbreakers Capturing human axial progenitors in vitro |